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