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