Theorem cos3t

Description: Triple-angle formula for cosine, in pure cosine form. (Contributed by Ender Ting, 16-Mar-2026)

	Ref	Expression
Assertion	cos3t	$$⊢A\in ℂ\to \cos 3A=4{\cos A}^3-3\cos A$$

Proof

Step	Hyp	Ref	Expression
1		df-3	$$⊢3=2+1$$
2	1	oveq1i	$$⊢3A=\left(2+1\right)A$$
3		2cnd	$$⊢A\in ℂ\to 2\in ℂ$$
4		1cnd	$$⊢A\in ℂ\to 1\in ℂ$$
5		id	$$⊢A\in ℂ\to A\in ℂ$$
6	3 4 5	adddird	$$⊢A\in ℂ\to \left(2+1\right)A=2A+1A$$
7	2 6	eqtrid	$$⊢A\in ℂ\to 3A=2A+1A$$
8	7	fveq2d	$$⊢A\in ℂ\to \cos 3A=\cos \left(2A+1A\right)$$
9	3 5	mulcld	$$⊢A\in ℂ\to 2A\in ℂ$$
10	4 5	mulcld	$$⊢A\in ℂ\to 1A\in ℂ$$
11		cosadd	$$⊢\left(2A\in ℂ\wedge 1A\in ℂ\right)\to \cos \left(2A+1A\right)=\cos 2A\cos 1A-\sin 2A\sin 1A$$
12	9 10 11	syl2anc	$$⊢A\in ℂ\to \cos \left(2A+1A\right)=\cos 2A\cos 1A-\sin 2A\sin 1A$$
13		cos2t	$$⊢A\in ℂ\to \cos 2A=2{\cos A}^2-1$$
14		mullid	$$⊢A\in ℂ\to 1A=A$$
15	14	fveq2d	$$⊢A\in ℂ\to \cos 1A=\cos A$$
16	13 15	oveq12d	$$⊢A\in ℂ\to \cos 2A\cos 1A=\left(2{\cos A}^2-1\right)\cos A$$
17		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
18	17	sqcld	$$⊢A\in ℂ\to {\cos A}^2\in ℂ$$
19	3 18	mulcld	$$⊢A\in ℂ\to 2{\cos A}^2\in ℂ$$
20	19 4 17	subdird	$$⊢A\in ℂ\to \left(2{\cos A}^2-1\right)\cos A=2{\cos A}^2\cos A-1\cos A$$
21	3 18 17	mulassd	$$⊢A\in ℂ\to 2{\cos A}^2\cos A=2{\cos A}^2\cos A$$
22	1	oveq2i	$$⊢{\cos A}^3={\cos A}^{2+1}$$
23		2nn0	$$⊢2\in {\mathbb{N}}_0$$
24	23	a1i	$$⊢A\in ℂ\to 2\in {\mathbb{N}}_0$$
25	17 24	expp1d	$$⊢A\in ℂ\to {\cos A}^{2+1}={\cos A}^2\cos A$$
26	22 25	eqtr2id	$$⊢A\in ℂ\to {\cos A}^2\cos A={\cos A}^3$$
27	26	oveq2d	$$⊢A\in ℂ\to 2{\cos A}^2\cos A=2{\cos A}^3$$
28	21 27	eqtrd	$$⊢A\in ℂ\to 2{\cos A}^2\cos A=2{\cos A}^3$$
29	28	oveq1d	$$⊢A\in ℂ\to 2{\cos A}^2\cos A-1\cos A=2{\cos A}^3-1\cos A$$
30	16 20 29	3eqtrd	$$⊢A\in ℂ\to \cos 2A\cos 1A=2{\cos A}^3-1\cos A$$
31		sin2t	$$⊢A\in ℂ\to \sin 2A=2\sin A\cos A$$
32	14	fveq2d	$$⊢A\in ℂ\to \sin 1A=\sin A$$
33	31 32	oveq12d	$$⊢A\in ℂ\to \sin 2A\sin 1A=2\sin A\cos A\sin A$$
34		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
35	34 17	mulcld	$$⊢A\in ℂ\to \sin A\cos A\in ℂ$$
36	3 35 34	mulassd	$$⊢A\in ℂ\to 2\sin A\cos A\sin A=2\sin A\cos A\sin A$$
37	34 17 34	mulassd	$$⊢A\in ℂ\to \sin A\cos A\sin A=\sin A\cos A\sin A$$
38	34 17 34	mul12d	$$⊢A\in ℂ\to \sin A\cos A\sin A=\cos A\sin A\sin A$$
39	34	sqvald	$$⊢A\in ℂ\to {\sin A}^2=\sin A\sin A$$
40	39	eqcomd	$$⊢A\in ℂ\to \sin A\sin A={\sin A}^2$$
41	40	oveq2d	$$⊢A\in ℂ\to \cos A\sin A\sin A=\cos A{\sin A}^2$$
42	37 38 41	3eqtrd	$$⊢A\in ℂ\to \sin A\cos A\sin A=\cos A{\sin A}^2$$
43	34	sqcld	$$⊢A\in ℂ\to {\sin A}^2\in ℂ$$
44		sincossq	$$⊢A\in ℂ\to {\sin A}^2+{\cos A}^2=1$$
45	43 18 44	mvlraddd	$$⊢A\in ℂ\to {\sin A}^2=1-{\cos A}^2$$
46	45	oveq2d	$$⊢A\in ℂ\to \cos A{\sin A}^2=\cos A\left(1-{\cos A}^2\right)$$
47	17 4 18	subdid	$$⊢A\in ℂ\to \cos A\left(1-{\cos A}^2\right)=\cos A\cdot 1-\cos A{\cos A}^2$$
48	17	mulridd	$$⊢A\in ℂ\to \cos A\cdot 1=\cos A$$
49	1	a1i	$$⊢A\in ℂ\to 3=2+1$$
50	49	oveq2d	$$⊢A\in ℂ\to {\cos A}^3={\cos A}^{2+1}$$
51	18 17	mulcomd	$$⊢A\in ℂ\to {\cos A}^2\cos A=\cos A{\cos A}^2$$
52	50 25 51	3eqtrrd	$$⊢A\in ℂ\to \cos A{\cos A}^2={\cos A}^3$$
53	48 52	oveq12d	$$⊢A\in ℂ\to \cos A\cdot 1-\cos A{\cos A}^2=\cos A-{\cos A}^3$$
54	47 53	eqtrd	$$⊢A\in ℂ\to \cos A\left(1-{\cos A}^2\right)=\cos A-{\cos A}^3$$
55	42 46 54	3eqtrd	$$⊢A\in ℂ\to \sin A\cos A\sin A=\cos A-{\cos A}^3$$
56	55	oveq2d	$$⊢A\in ℂ\to 2\sin A\cos A\sin A=2\left(\cos A-{\cos A}^3\right)$$
57	36 56	eqtrd	$$⊢A\in ℂ\to 2\sin A\cos A\sin A=2\left(\cos A-{\cos A}^3\right)$$
58		3nn0	$$⊢3\in {\mathbb{N}}_0$$
59	58	a1i	$$⊢A\in ℂ\to 3\in {\mathbb{N}}_0$$
60	17 59	expcld	$$⊢A\in ℂ\to {\cos A}^3\in ℂ$$
61	3 17 60	subdid	$$⊢A\in ℂ\to 2\left(\cos A-{\cos A}^3\right)=2\cos A-2{\cos A}^3$$
62	33 57 61	3eqtrd	$$⊢A\in ℂ\to \sin 2A\sin 1A=2\cos A-2{\cos A}^3$$
63	30 62	oveq12d	$$⊢A\in ℂ\to \cos 2A\cos 1A-\sin 2A\sin 1A=2{\cos A}^3-1\cos A-\left(2\cos A-2{\cos A}^3\right)$$
64	3 60	mulcld	$$⊢A\in ℂ\to 2{\cos A}^3\in ℂ$$
65	4 17	mulcld	$$⊢A\in ℂ\to 1\cos A\in ℂ$$
66	3 17	mulcld	$$⊢A\in ℂ\to 2\cos A\in ℂ$$
67	64 65 66 64	subadd4d	$$⊢A\in ℂ\to 2{\cos A}^3-1\cos A-\left(2\cos A-2{\cos A}^3\right)=2{\cos A}^3+2{\cos A}^3-\left(1\cos A+2\cos A\right)$$
68	3 3 60	adddird	$$⊢A\in ℂ\to \left(2+2\right){\cos A}^3=2{\cos A}^3+2{\cos A}^3$$
69		2p2e4	$$⊢2+2=4$$
70	69	a1i	$$⊢A\in ℂ\to 2+2=4$$
71	70	oveq1d	$$⊢A\in ℂ\to \left(2+2\right){\cos A}^3=4{\cos A}^3$$
72	68 71	eqtr3d	$$⊢A\in ℂ\to 2{\cos A}^3+2{\cos A}^3=4{\cos A}^3$$
73	4 3 17	adddird	$$⊢A\in ℂ\to \left(1+2\right)\cos A=1\cos A+2\cos A$$
74		1p2e3	$$⊢1+2=3$$
75	74	a1i	$$⊢A\in ℂ\to 1+2=3$$
76	75	oveq1d	$$⊢A\in ℂ\to \left(1+2\right)\cos A=3\cos A$$
77	73 76	eqtr3d	$$⊢A\in ℂ\to 1\cos A+2\cos A=3\cos A$$
78	72 77	oveq12d	$$⊢A\in ℂ\to 2{\cos A}^3+2{\cos A}^3-\left(1\cos A+2\cos A\right)=4{\cos A}^3-3\cos A$$
79	63 67 78	3eqtrd	$$⊢A\in ℂ\to \cos 2A\cos 1A-\sin 2A\sin 1A=4{\cos A}^3-3\cos A$$
80	8 12 79	3eqtrd	$$⊢A\in ℂ\to \cos 3A=4{\cos A}^3-3\cos A$$