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