HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem addsint 7399
Description: Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
Assertion
Ref Expression
addsint |- ((A e. CC /\ B e. CC) -> ((sin` A) + (sin` B)) = (2 x. ((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2)))))
Proof of Theorem addsint
StepHypRef Expression
1 axmulcl 5245 . . . 4 |- (((sin` ((A + B) / 2)) e. CC /\ (cos` ((A - B) / 2)) e. CC) -> ((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC)
2 axaddcl 5243 . . . . . 6 |- ((A e. CC /\ B e. CC) -> (A + B) e. CC)
3 halfclt 5980 . . . . . 6 |- ((A + B) e. CC -> ((A + B) / 2) e. CC)
42, 3syl 10 . . . . 5 |- ((A e. CC /\ B e. CC) -> ((A + B) / 2) e. CC)
5 sinclt 7373 . . . . 5 |- (((A + B) / 2) e. CC -> (sin` ((A + B) / 2)) e. CC)
64, 5syl 10 . . . 4 |- ((A e. CC /\ B e. CC) -> (sin` ((A + B) / 2)) e. CC)
7 subclt 5339 . . . . . 6 |- ((A e. CC /\ B e. CC) -> (A - B) e. CC)
8 halfclt 5980 . . . . . 6 |- ((A - B) e. CC -> ((A - B) / 2) e. CC)
97, 8syl 10 . . . . 5 |- ((A e. CC /\ B e. CC) -> ((A - B) / 2) e. CC)
10 cosclt 7374 . . . . 5 |- (((A - B) / 2) e. CC -> (cos` ((A - B) / 2)) e. CC)
119, 10syl 10 . . . 4 |- ((A e. CC /\ B e. CC) -> (cos` ((A - B) / 2)) e. CC)
121, 6, 11sylanc 471 . . 3 |- ((A e. CC /\ B e. CC) -> ((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC)
13 2timest 5951 . . 3 |- (((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2))) e. CC -> (2 x. ((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2)))) = (((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2)))))
1412, 13syl 10 . 2 |- ((A e. CC /\ B e. CC) -> (2 x. ((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2)))) = (((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2)))))
15 sinaddt 7395 . . . . 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)))))
1615, 4, 9sylanc 471 . . . 4 |- ((A e. CC /\ B 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)))))
17 sinsubt 7397 . . . . 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)))))
1817, 4, 9sylanc 471 . . . 4 |- ((A e. CC /\ B 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)))))
1916, 18opreq12d 3963 . . 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))))))
20 ppncant 5453 . . . 4 |- ((((sin` ((A + B) / 2)) x. (cos` ((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))) 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))))) = (((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2)))))
21 axmulcl 5245 . . . . 5 |- (((cos` ((A + B) / 2)) e. CC /\ (sin` ((A - B) / 2)) e. CC) -> ((cos` ((A + B) / 2)) x. (sin` ((A - B) / 2))) e. CC)
22 cosclt 7374 . . . . . 6 |- (((A + B) / 2) e. CC -> (cos` ((A + B) / 2)) e. CC)
234, 22syl 10 . . . . 5 |- ((A e. CC /\ B e. CC) -> (cos` ((A + B) / 2)) e. CC)
24 sinclt 7373 . . . . . 6 |- (((A - B) / 2) e. CC -> (sin` ((A - B) / 2)) e. CC)
259, 24syl 10 . . . . 5 |- ((A e. CC /\ B e. CC) -> (sin` ((A - B) / 2)) e. CC)
2621, 23, 25sylanc 471 . . . 4 |- ((A e. CC /\ B e. CC) -> ((cos` ((A + B) / 2)) x. (sin` ((A - B) / 2))) e. CC)
2720, 12, 26, 12syl3anc 856 . . 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))))) = (((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2))) + ((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2)))))
2819, 27eqtrd 1499 . 2 |- ((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))) + ((sin` ((A + B) / 2)) x. (cos` ((A - B) / 2)))))
29 halfaddsubt 5988 . . . . 5 |- ((A e. CC /\ B e. CC) -> ((((A + B) / 2) + ((A - B) / 2)) =