Metamath Proof Explorer

Theorem subsin

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

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

Proof

Step Hyp Ref Expression
1 halfaddsubcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) / 2 ) e. CC /\ ( ( A - B ) / 2 ) e. CC ) )
2 coscl 
 |-  ( ( ( A + B ) / 2 ) e. CC -> ( cos ` ( ( A + B ) / 2 ) ) e. CC )
3 sincl 
 |-  ( ( ( A - B ) / 2 ) e. CC -> ( sin ` ( ( A - B ) / 2 ) ) e. CC )
4 mulcl 
 |-  ( ( ( cos ` ( ( A + B ) / 2 ) ) e. CC /\ ( sin ` ( ( A - B ) / 2 ) ) e. CC ) -> ( ( cos ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) e. CC )
5 2 3 4 syl2an 
 |-  ( ( ( ( A + B ) / 2 ) e. CC /\ ( ( A - B ) / 2 ) e. CC ) -> ( ( cos ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) e. CC )
6 1 5 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) e. CC )
7 6 2timesd 
 |-  ( ( 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 ) ) ) ) )
8 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 ) ) ) ) )
9 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 ) ) ) ) )
10 8 9 oveq12d 
 |-  ( ( ( ( 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 ) ) ) ) ) )
11 1 10 syl 
 |-  ( ( 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 ) ) ) ) ) )
12 sincl 
 |-  ( ( ( A + B ) / 2 ) e. CC -> ( sin ` ( ( A + B ) / 2 ) ) e. CC )
13 coscl 
 |-  ( ( ( A - B ) / 2 ) e. CC -> ( cos ` ( ( A - B ) / 2 ) ) e. CC )
14 mulcl 
 |-  ( ( ( sin ` ( ( A + B ) / 2 ) ) e. CC /\ ( cos ` ( ( A - B ) / 2 ) ) e. CC ) -> ( ( sin ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) e. CC )
15 12 13 14 syl2an 
 |-  ( ( ( ( A + B ) / 2 ) e. CC /\ ( ( A - B ) / 2 ) e. CC ) -> ( ( sin ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) e. CC )
16 1 15 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) e. CC )
17 16 6 6 pnncand 
 |-  ( ( 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 ) ) ) ) )
18 11 17 eqtrd 
 |-  ( ( 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 ) ) ) ) )
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 7 18 24 3eqtr2rd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) - ( sin ` B ) ) = ( 2 x. ( ( cos ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )