HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem subcost 7460
Description: Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
Assertion
Ref Expression
subcost |- ((A e. CC /\ B e. CC) -> ((cos` A) - (cos` B)) = (-u2 x. ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))))
Proof of Theorem subcost
StepHypRef Expression
1 halfaddsubcl 6040 . . . . . 6 |- ((A e. CC /\ B e. CC) -> (((A + B) / 2) e. CC /\ ((A - B) / 2) e. CC))
2 axmulcl 5273 . . . . . . 7 |- (((sin` ((A + B) / 2)) e. CC /\ (sin` ((A - B) / 2)) e. CC) -> ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) e. CC)
3 sinclt 7431 . . . . . . 7 |- (((A + B) / 2) e. CC -> (sin` ((A + B) / 2)) e. CC)
4 sinclt 7431 . . . . . . 7 |- (((A - B) / 2) e. CC -> (sin` ((A - B) / 2)) e. CC)
52, 3, 4syl2an 454 . . . . . 6 |- ((((A + B) / 2) e. CC /\ ((A - B) / 2) e. CC) -> ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) e. CC)
61, 5syl 10 . . . . 5 |- ((A e. CC /\ B e. CC) -> ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) e. CC)
7 2timest 6004 . . . . 5 |- (((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) e. CC -> (2 x. ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))) = (((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))))
86, 7syl 10 . . . 4 |- ((A e. CC /\ B e. CC) -> (2 x. ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))) = (((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))))
9 cossubt 7456 . . . . . . 7 |- ((((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)))))
10 cosaddt 7454 . . . . . . 7 |- ((((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)))))
119, 10opreq12d 3978 . . . . . 6 |- ((((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))))))
121, 11syl 10 . . . . 5 |- ((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))))))
13 pnncant 5480 . . . . . 6 |- ((((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC /\ ((sin` ((A + B) / 2)) x. (sin` ((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))) + ((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))))) = (((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))))
14 axmulcl 5273 . . . . . . . 8 |- (((cos` ((A + B) / 2)) e. CC /\ (cos` ((A - B) / 2)) e. CC) -> ((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC)
15 cosclt 7432 . . . . . . . 8 |- (((A + B) / 2) e. CC -> (cos` ((A + B) / 2)) e. CC)
16 cosclt 7432 . . . . . . . 8 |- (((A - B) / 2) e. CC -> (cos` ((A - B) / 2)) e. CC)
1714, 15, 16syl2an 454 . . . . . . 7 |- ((((A + B) / 2) e. CC /\ ((A - B) / 2) e. CC) -> ((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC)
181, 17syl 10 . . . . . 6 |- ((A e. CC /\ B e. CC) -> ((cos` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC)
1913, 18, 6, 6syl3anc 858 . . . . 5 |- ((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))))) = (((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))))
2012, 19eqtrd 1507 . . . 4 |- ((A e. CC /\ B e. CC) -> ((cos` (((A + B) / 2) - ((A - B) / 2))) - (cos` (((A + B) / 2) + ((A - B) / 2)))) = (((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (sin` ((A - B) / 2)))))
21 halfaddsubt 6041 . . . . . . . 8 |- ((A e. CC /\ B e. CC) -> ((((A + B) / 2) + ((A - B) / 2)) = A /\ (((A + B) / 2) - ((A - B) / 2)) = B))
2221pm3.27d 325 . . . . . . 7 |- ((A e. CC /\ B e. CC) -> (((A + B) / 2) - ((A - B) / 2)) = B)
2322fveq2d 3728 . . . . . 6 |- ((A e. CC /\ B e. CC) -> (cos` (((A + B) / 2) - ((A - B) / 2))) = (cos`