HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem addcost 7409
Description: Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
Assertion
Ref Expression
addcost |- ((A e. CC /\ B e. CC) -> ((cos` A) + (cos` B)) = (2 x. ((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2)))))
Proof of Theorem addcost
StepHypRef Expression
1 axaddcom 5255 . . 3 |- (((cos` A) e. CC /\ (cos` B) e. CC) -> ((cos` A) + (cos` B)) = ((cos` B) + (cos` A)))
2 cosclt 7382 . . 3 |- (A e. CC -> (cos` A) e. CC)
3 cosclt 7382 . . 3 |- (B e. CC -> (cos` B) e. CC)
41, 2, 3syl2an 454 . 2 |- ((A e. CC /\ B e. CC) -> ((cos` A) + (cos` B)) = ((cos` B) + (cos` A)))
5 halfaddsubt 5996 . . . . 5 |- ((A e. CC /\ B e. CC) -> ((((A + B) / 2) + ((A - B) / 2)) = A /\ (((A + B) / 2) - ((A - B) / 2)) = B))
65pm3.27d 325 . . . 4 |- ((A e. CC /\ B e. CC) -> (((A + B) / 2) - ((A - B) / 2)) = B)
76fveq2d 3719 . . 3 |- ((A e. CC /\ B e. CC) -> (cos` (((A + B) / 2) - ((A - B) / 2))) = (cos` B))
85pm3.26d 321 . . . 4 |- ((A e. CC /\ B e. CC) -> (((A + B) / 2) + ((A - B) / 2)) = A)
98fveq2d 3719 . . 3 |- ((A e. CC /\ B e. CC) -> (cos` (((A + B) / 2) + ((A - B) / 2))) = (cos` A))
107, 9opreq12d 3969 . 2 |- ((A e. CC /\ B e. CC) -> ((cos` (((A + B) / 2) - ((A - B) / 2))) + (cos` (((A + B) / 2) + ((A - B) / 2)))) = ((cos` B) + (cos` A)))
11 ppncant 5461 . . . 4 |- ((((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC /\ ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) e. CC /\ ((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC) -> ((((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))) + (((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) - ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))))) = (((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) + ((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2)))))
12 halfaddsubcl 5995 . . . . 5 |- ((A e. CC /\ B e. CC) -> (((A + B) / 2) e. CC /\ ((A - B) / 2) e. CC))
13 axmulcl 5253 . . . . . 6 |- (((cos` ((A + B) / 2)) e. CC /\ (cos` ((A - B) / 2)) e. CC) -> ((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC)
14 cosclt 7382 . . . . . 6 |- (((A + B) / 2) e. CC -> (cos` ((A + B) / 2)) e. CC)
15 cosclt 7382 . . . . . 6 |- (((A - B) / 2) e. CC -> (cos` ((A - B) / 2)) e. CC)
1613, 14, 15syl2an 454 . . . . 5 |- ((((A + B) / 2) e. CC /\ ((A - B) / 2) e. CC) -> ((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC)
1712, 16syl 10 . . . 4 |- ((A e. CC /\ B e. CC) -> ((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC)
18 axmulcl 5253 . . . . . 6 |- (((sin` ((A + B) / 2)) e. CC /\ (sin` ((A - B) / 2)) e. CC) -> ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) e. CC)
19 sinclt 7381 . . . . . 6 |- (((A + B) / 2) e. CC -> (sin` ((A + B) / 2)) e. CC)
20 sinclt 7381 . . . . . 6 |- (((A - B) / 2) e. CC -> (sin` ((A - B) / 2)) e. CC)
2118, 19, 20syl2an 454 . . . . 5 |- ((((A + B) / 2) e. CC /\ ((A - B) / 2) e. CC) -> ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) e. CC)
2212, 21syl 10 . . . 4 |- ((A e. CC /\ B e. CC) -> ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) e. CC)
2311, 17, 22, 17syl3anc 857 . . 3 |- ((A e. CC /\ B e. CC) -> ((((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))) + (((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) - ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))))) = (((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) + ((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2)))))
24 cossubt 7406 . . . . 5 |- ((((A + B) / 2) e. CC /\ ((A - B) / 2) e. CC) -> (cos` (((A + B) / 2) - ((A - B) / 2))) = (((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))))
25 cosaddt 7404 . . . . 5 |- ((((A + B) / 2) e. CC /\ ((A - B) / 2) e. CC) -> (cos` (((A + B) / 2) + ((A - B) / 2))) = (((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) - ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))))
2624, 25opreq12d 3969 . . . 4 |- ((((A + B) / 2) e. CC /\ ((A - B) / 2) e. CC) -> ((cos` (((A + B) / 2) - ((A - B) / 2))) + (cos` (((A + B) / 2) + ((A - B) / 2)))) = ((((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))) + (((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) - ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))))))
2712, 26syl 10 . . 3 |- ((A e. CC /\ B e. CC) -> ((cos` (((A + B) / 2) - ((A - B) / 2))) + (cos` (((A + B) / 2) + ((A - B) / 2)))) = ((((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))) + (((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) - ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))))))
28 2timest 5959 . . . 4 |- (((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC -> (2 x. ((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2)))) = (