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	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \sin A\sin B=\frac{\cos \left(A-B\right)-\cos \left(A+B\right)}{2}$$

Proof

Step	Hyp	Ref	Expression
1		cossub	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \cos \left(A-B\right)=\cos A\cos B+\sin A\sin B$$
2		cosadd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \cos \left(A+B\right)=\cos A\cos B-\sin A\sin B$$
3	1 2	oveq12d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \cos \left(A-B\right)-\cos \left(A+B\right)=\cos A\cos B+\sin A\sin B-\left(\cos A\cos B-\sin A\sin B\right)$$
4		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
5		coscl	$$⊢B\in ℂ\to \cos B\in ℂ$$
6		mulcl	$$⊢\left(\cos A\in ℂ\wedge \cos B\in ℂ\right)\to \cos A\cos B\in ℂ$$
7	4 5 6	syl2an	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \cos A\cos B\in ℂ$$
8		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
9		sincl	$$⊢B\in ℂ\to \sin B\in ℂ$$
10		mulcl	$$⊢\left(\sin A\in ℂ\wedge \sin B\in ℂ\right)\to \sin A\sin B\in ℂ$$
11	8 9 10	syl2an	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \sin A\sin B\in ℂ$$
12		pnncan	$$⊢\left(\cos A\cos B\in ℂ\wedge \sin A\sin B\in ℂ\wedge \sin A\sin B\in ℂ\right)\to \cos A\cos B+\sin A\sin B-\left(\cos A\cos B-\sin A\sin B\right)=\sin A\sin B+\sin A\sin B$$
13	12	3anidm23	$$⊢\left(\cos A\cos B\in ℂ\wedge \sin A\sin B\in ℂ\right)\to \cos A\cos B+\sin A\sin B-\left(\cos A\cos B-\sin A\sin B\right)=\sin A\sin B+\sin A\sin B$$
14		2times	$$⊢\sin A\sin B\in ℂ\to 2\sin A\sin B=\sin A\sin B+\sin A\sin B$$
15	14	adantl	$$⊢\left(\cos A\cos B\in ℂ\wedge \sin A\sin B\in ℂ\right)\to 2\sin A\sin B=\sin A\sin B+\sin A\sin B$$
16	13 15	eqtr4d	$$⊢\left(\cos A\cos B\in ℂ\wedge \sin A\sin B\in ℂ\right)\to \cos A\cos B+\sin A\sin B-\left(\cos A\cos B-\sin A\sin B\right)=2\sin A\sin B$$
17	7 11 16	syl2anc	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \cos A\cos B+\sin A\sin B-\left(\cos A\cos B-\sin A\sin B\right)=2\sin A\sin B$$
18		2cn	$$⊢2\in ℂ$$
19		mulcom	$$⊢\left(2\in ℂ\wedge \sin A\sin B\in ℂ\right)\to 2\sin A\sin B=\sin A\sin B\cdot 2$$
20	18 11 19	sylancr	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to 2\sin A\sin B=\sin A\sin B\cdot 2$$
21	3 17 20	3eqtrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \cos \left(A-B\right)-\cos \left(A+B\right)=\sin A\sin B\cdot 2$$
22	21	oveq1d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \frac{\cos \left(A-B\right)-\cos \left(A+B\right)}{2}=\frac{\sin A\sin B\cdot 2}{2}$$
23		2ne0	$$⊢2\ne 0$$
24		divcan4	$$⊢\left(\sin A\sin B\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to \frac{\sin A\sin B\cdot 2}{2}=\sin A\sin B$$
25	18 23 24	mp3an23	$$⊢\sin A\sin B\in ℂ\to \frac{\sin A\sin B\cdot 2}{2}=\sin A\sin B$$
26	11 25	syl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \frac{\sin A\sin B\cdot 2}{2}=\sin A\sin B$$
27	22 26	eqtr2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \sin A\sin B=\frac{\cos \left(A-B\right)-\cos \left(A+B\right)}{2}$$