cos3t

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

		Ref	Expression
	Assertion	cos3t	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 3 · 𝐴 ) ) = ( ( 4 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) − ( 3 · ( cos ‘ 𝐴 ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem cos3t

Proof