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