Theorem cos2t

Description: Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008)

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

Proof

Step	Hyp	Ref	Expression
1		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
2	1	sqcld	$$⊢A\in ℂ\to {\cos A}^2\in ℂ$$
3		ax-1cn	$$⊢1\in ℂ$$
4		subsub3	$$⊢\left({\cos A}^2\in ℂ\wedge 1\in ℂ\wedge {\cos A}^2\in ℂ\right)\to {\cos A}^2-\left(1-{\cos A}^2\right)={\cos A}^2+{\cos A}^2-1$$
5	3 4	mp3an2	$$⊢\left({\cos A}^2\in ℂ\wedge {\cos A}^2\in ℂ\right)\to {\cos A}^2-\left(1-{\cos A}^2\right)={\cos A}^2+{\cos A}^2-1$$
6	2 2 5	syl2anc	$$⊢A\in ℂ\to {\cos A}^2-\left(1-{\cos A}^2\right)={\cos A}^2+{\cos A}^2-1$$
7		cosadd	$$⊢\left(A\in ℂ\wedge A\in ℂ\right)\to \cos \left(A+A\right)=\cos A\cos A-\sin A\sin A$$
8	7	anidms	$$⊢A\in ℂ\to \cos \left(A+A\right)=\cos A\cos A-\sin A\sin A$$
9		2times	$$⊢A\in ℂ\to 2A=A+A$$
10	9	fveq2d	$$⊢A\in ℂ\to \cos 2A=\cos \left(A+A\right)$$
11	1	sqvald	$$⊢A\in ℂ\to {\cos A}^2=\cos A\cos A$$
12		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
13	12	sqvald	$$⊢A\in ℂ\to {\sin A}^2=\sin A\sin A$$
14	11 13	oveq12d	$$⊢A\in ℂ\to {\cos A}^2-{\sin A}^2=\cos A\cos A-\sin A\sin A$$
15	8 10 14	3eqtr4d	$$⊢A\in ℂ\to \cos 2A={\cos A}^2-{\sin A}^2$$
16	12	sqcld	$$⊢A\in ℂ\to {\sin A}^2\in ℂ$$
17	16 2	addcomd	$$⊢A\in ℂ\to {\sin A}^2+{\cos A}^2={\cos A}^2+{\sin A}^2$$
18		sincossq	$$⊢A\in ℂ\to {\sin A}^2+{\cos A}^2=1$$
19	17 18	eqtr3d	$$⊢A\in ℂ\to {\cos A}^2+{\sin A}^2=1$$
20		subadd	$$⊢\left(1\in ℂ\wedge {\cos A}^2\in ℂ\wedge {\sin A}^2\in ℂ\right)\to \left(1-{\cos A}^2={\sin A}^2\leftrightarrow {\cos A}^2+{\sin A}^2=1\right)$$
21	3 2 16 20	mp3an2i	$$⊢A\in ℂ\to \left(1-{\cos A}^2={\sin A}^2\leftrightarrow {\cos A}^2+{\sin A}^2=1\right)$$
22	19 21	mpbird	$$⊢A\in ℂ\to 1-{\cos A}^2={\sin A}^2$$
23	22	oveq2d	$$⊢A\in ℂ\to {\cos A}^2-\left(1-{\cos A}^2\right)={\cos A}^2-{\sin A}^2$$
24	15 23	eqtr4d	$$⊢A\in ℂ\to \cos 2A={\cos A}^2-\left(1-{\cos A}^2\right)$$
25	2	2timesd	$$⊢A\in ℂ\to 2{\cos A}^2={\cos A}^2+{\cos A}^2$$
26	25	oveq1d	$$⊢A\in ℂ\to 2{\cos A}^2-1={\cos A}^2+{\cos A}^2-1$$
27	6 24 26	3eqtr4d	$$⊢A\in ℂ\to \cos 2A=2{\cos A}^2-1$$