Step |
Hyp |
Ref |
Expression |
1 |
|
addcl |
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC ) |
2 |
1
|
halfcld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) / 2 ) e. CC ) |
3 |
2
|
sincld |
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` ( ( A + B ) / 2 ) ) e. CC ) |
4 |
|
subcl |
|- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC ) |
5 |
4
|
halfcld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) / 2 ) e. CC ) |
6 |
5
|
coscld |
|- ( ( A e. CC /\ B e. CC ) -> ( cos ` ( ( A - B ) / 2 ) ) e. CC ) |
7 |
3 6
|
mulcld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) e. CC ) |
8 |
7
|
2timesd |
|- ( ( 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 ) ) ) ) ) |
9 |
|
sinadd |
|- ( ( ( ( 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 |
2 5 9
|
syl2anc |
|- ( ( 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 ) ) ) ) ) |
11 |
|
sinsub |
|- ( ( ( ( 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 ) ) ) ) ) |
12 |
2 5 11
|
syl2anc |
|- ( ( 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 ) ) ) ) ) |
13 |
10 12
|
oveq12d |
|- ( ( 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 ) ) ) ) ) ) |
14 |
2
|
coscld |
|- ( ( A e. CC /\ B e. CC ) -> ( cos ` ( ( A + B ) / 2 ) ) e. CC ) |
15 |
5
|
sincld |
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` ( ( A - B ) / 2 ) ) e. CC ) |
16 |
14 15
|
mulcld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) e. CC ) |
17 |
7 16 7
|
ppncand |
|- ( ( 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 ) ) ) ) ) |
18 |
13 17
|
eqtrd |
|- ( ( 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 ) ) ) ) ) |
19 |
|
halfaddsub |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) = A /\ ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) = B ) ) |
20 |
19
|
simpld |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) = A ) |
21 |
20
|
fveq2d |
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) ) = ( sin ` A ) ) |
22 |
19
|
simprd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) = B ) |
23 |
22
|
fveq2d |
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) ) = ( sin ` B ) ) |
24 |
21 23
|
oveq12d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) ) + ( sin ` ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) ) ) = ( ( sin ` A ) + ( sin ` B ) ) ) |
25 |
8 18 24
|
3eqtr2rd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) + ( sin ` B ) ) = ( 2 x. ( ( sin ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) ) ) |