Metamath Proof Explorer

Theorem addsin

Description: Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007)

Ref Expression
Assertion addsin 
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) + ( sin ` B ) ) = ( 2 x. ( ( sin ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) ) )

Proof

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 ) ) ) ) )