This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sinmul

Description: Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd and cossub . (Contributed by David A. Wheeler, 26-May-2015)

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

Proof

Step Hyp Ref Expression
1 cossub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A - B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) )
2 cosadd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A + B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) )
3 1 2 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` ( A - B ) ) - ( cos ` ( A + B ) ) ) = ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) - ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) ) )
4 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
5 coscl 
 |-  ( B e. CC -> ( cos ` B ) e. CC )
6 mulcl 
 |-  ( ( ( cos ` A ) e. CC /\ ( cos ` B ) e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) e. CC )
7 4 5 6 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) e. CC )
8 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
9 sincl 
 |-  ( B e. CC -> ( sin ` B ) e. CC )
10 mulcl 
 |-  ( ( ( sin ` A ) e. CC /\ ( sin ` B ) e. CC ) -> ( ( sin ` A ) x. ( sin ` B ) ) e. CC )
11 8 9 10 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( sin ` B ) ) e. CC )
12 pnncan 
 |-  ( ( ( ( cos ` A ) x. ( cos ` B ) ) e. CC /\ ( ( sin ` A ) x. ( sin ` B ) ) e. CC /\ ( ( sin ` A ) x. ( sin ` B ) ) e. CC ) -> ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) - ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) ) = ( ( ( sin ` A ) x. ( sin ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) )
13 12 3anidm23 
 |-  ( ( ( ( cos ` A ) x. ( cos ` B ) ) e. CC /\ ( ( sin ` A ) x. ( sin ` B ) ) e. CC ) -> ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) - ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) ) = ( ( ( sin ` A ) x. ( sin ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) )
14 2times 
 |-  ( ( ( sin ` A ) x. ( sin ` B ) ) e. CC -> ( 2 x. ( ( sin ` A ) x. ( sin ` B ) ) ) = ( ( ( sin ` A ) x. ( sin ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) )
15 14 adantl 
 |-  ( ( ( ( cos ` A ) x. ( cos ` B ) ) e. CC /\ ( ( sin ` A ) x. ( sin ` B ) ) e. CC ) -> ( 2 x. ( ( sin ` A ) x. ( sin ` B ) ) ) = ( ( ( sin ` A ) x. ( sin ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) )
16 13 15 eqtr4d 
 |-  ( ( ( ( cos ` A ) x. ( cos ` B ) ) e. CC /\ ( ( sin ` A ) x. ( sin ` B ) ) e. CC ) -> ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) - ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) ) = ( 2 x. ( ( sin ` A ) x. ( sin ` B ) ) ) )
17 7 11 16 syl2anc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) - ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) ) = ( 2 x. ( ( sin ` A ) x. ( sin ` B ) ) ) )
18 2cn 
 |-  2 e. CC
19 mulcom 
 |-  ( ( 2 e. CC /\ ( ( sin ` A ) x. ( sin ` B ) ) e. CC ) -> ( 2 x. ( ( sin ` A ) x. ( sin ` B ) ) ) = ( ( ( sin ` A ) x. ( sin ` B ) ) x. 2 ) )
20 18 11 19 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( ( sin ` A ) x. ( sin ` B ) ) ) = ( ( ( sin ` A ) x. ( sin ` B ) ) x. 2 ) )
21 3 17 20 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` ( A - B ) ) - ( cos ` ( A + B ) ) ) = ( ( ( sin ` A ) x. ( sin ` B ) ) x. 2 ) )
22 21 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` ( A - B ) ) - ( cos ` ( A + B ) ) ) / 2 ) = ( ( ( ( sin ` A ) x. ( sin ` B ) ) x. 2 ) / 2 ) )
23 2ne0 
 |-  2 =/= 0
24 divcan4 
 |-  ( ( ( ( sin ` A ) x. ( sin ` B ) ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( ( ( sin ` A ) x. ( sin ` B ) ) x. 2 ) / 2 ) = ( ( sin ` A ) x. ( sin ` B ) ) )
25 18 23 24 mp3an23 
 |-  ( ( ( sin ` A ) x. ( sin ` B ) ) e. CC -> ( ( ( ( sin ` A ) x. ( sin ` B ) ) x. 2 ) / 2 ) = ( ( sin ` A ) x. ( sin ` B ) ) )
26 11 25 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( sin ` A ) x. ( sin ` B ) ) x. 2 ) / 2 ) = ( ( sin ` A ) x. ( sin ` B ) ) )
27 22 26 eqtr2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( sin ` B ) ) = ( ( ( cos ` ( A - B ) ) - ( cos ` ( A + B ) ) ) / 2 ) )