Theorem cos2tsin

Description: Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008)

	Ref	Expression
Assertion	cos2tsin	$$⊢A\in ℂ\to \cos 2A=1-2{\sin A}^2$$

Proof

Step	Hyp	Ref	Expression
1		cos2t	$$⊢A\in ℂ\to \cos 2A=2{\cos A}^2-1$$
2		2cn	$$⊢2\in ℂ$$
3		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
4	3	sqcld	$$⊢A\in ℂ\to {\sin A}^2\in ℂ$$
5		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
6	5	sqcld	$$⊢A\in ℂ\to {\cos A}^2\in ℂ$$
7		adddi	$$⊢\left(2\in ℂ\wedge {\sin A}^2\in ℂ\wedge {\cos A}^2\in ℂ\right)\to 2\left({\sin A}^2+{\cos A}^2\right)=2{\sin A}^2+2{\cos A}^2$$
8	2 4 6 7	mp3an2i	$$⊢A\in ℂ\to 2\left({\sin A}^2+{\cos A}^2\right)=2{\sin A}^2+2{\cos A}^2$$
9		sincossq	$$⊢A\in ℂ\to {\sin A}^2+{\cos A}^2=1$$
10	9	oveq2d	$$⊢A\in ℂ\to 2\left({\sin A}^2+{\cos A}^2\right)=2\cdot 1$$
11	8 10	eqtr3d	$$⊢A\in ℂ\to 2{\sin A}^2+2{\cos A}^2=2\cdot 1$$
12		2t1e2	$$⊢2\cdot 1=2$$
13	11 12	eqtrdi	$$⊢A\in ℂ\to 2{\sin A}^2+2{\cos A}^2=2$$
14		mulcl	$$⊢\left(2\in ℂ\wedge {\sin A}^2\in ℂ\right)\to 2{\sin A}^2\in ℂ$$
15	2 4 14	sylancr	$$⊢A\in ℂ\to 2{\sin A}^2\in ℂ$$
16		mulcl	$$⊢\left(2\in ℂ\wedge {\cos A}^2\in ℂ\right)\to 2{\cos A}^2\in ℂ$$
17	2 6 16	sylancr	$$⊢A\in ℂ\to 2{\cos A}^2\in ℂ$$
18		subadd	$$⊢\left(2\in ℂ\wedge 2{\sin A}^2\in ℂ\wedge 2{\cos A}^2\in ℂ\right)\to \left(2-2{\sin A}^2=2{\cos A}^2\leftrightarrow 2{\sin A}^2+2{\cos A}^2=2\right)$$
19	2 15 17 18	mp3an2i	$$⊢A\in ℂ\to \left(2-2{\sin A}^2=2{\cos A}^2\leftrightarrow 2{\sin A}^2+2{\cos A}^2=2\right)$$
20	13 19	mpbird	$$⊢A\in ℂ\to 2-2{\sin A}^2=2{\cos A}^2$$
21	20	oveq1d	$$⊢A\in ℂ\to 2-2{\sin A}^2-1=2{\cos A}^2-1$$
22		ax-1cn	$$⊢1\in ℂ$$
23		sub32	$$⊢\left(2\in ℂ\wedge 2{\sin A}^2\in ℂ\wedge 1\in ℂ\right)\to 2-2{\sin A}^2-1=2-1-2{\sin A}^2$$
24	2 22 23	mp3an13	$$⊢2{\sin A}^2\in ℂ\to 2-2{\sin A}^2-1=2-1-2{\sin A}^2$$
25	15 24	syl	$$⊢A\in ℂ\to 2-2{\sin A}^2-1=2-1-2{\sin A}^2$$
26		2m1e1	$$⊢2-1=1$$
27	26	oveq1i	$$⊢2-1-2{\sin A}^2=1-2{\sin A}^2$$
28	25 27	eqtrdi	$$⊢A\in ℂ\to 2-2{\sin A}^2-1=1-2{\sin A}^2$$
29	1 21 28	3eqtr2d	$$⊢A\in ℂ\to \cos 2A=1-2{\sin A}^2$$