Theorem cos3t

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

	Ref	Expression
Assertion	cos3t	|- ( A e. CC -> ( cos ` ( 3 x. A ) ) = ( ( 4 x. ( ( cos ` A ) ^ 3 ) ) - ( 3 x. ( cos ` A ) ) ) )

Proof

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