Theorem cos5t

Description: Five-times-angle formula for cosine, in pure cosine form. (Contributed by Ender Ting, 20-Apr-2026)

	Ref	Expression
Assertion	cos5t	$$⊢A\in ℂ\to \cos 5A=16{\cos A}^5-20{\cos A}^3+5\cos A$$

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2		2cn	$$⊢2\in ℂ$$
3		2ne0	$$⊢2\ne 0$$
4	1 2 3	divcli	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ$$
5	4	a1i	$$⊢A\in ℂ\to \frac{\mathrm{\pi }}{2}\in ℂ$$
6		5cn	$$⊢5\in ℂ$$
7	6	a1i	$$⊢A\in ℂ\to 5\in ℂ$$
8		id	$$⊢A\in ℂ\to A\in ℂ$$
9	7 8	mulcld	$$⊢A\in ℂ\to 5A\in ℂ$$
10	5 9	subcld	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)-5A\in ℂ$$
11		1zzd	$$⊢A\in ℂ\to 1\in \mathbb{Z}$$
12		sinper	$$⊢\left(\left(\frac{\mathrm{\pi }}{2}\right)-5A\in ℂ\wedge 1\in \mathbb{Z}\right)\to \sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-5A+12\mathrm{\pi }\right)=\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-5A\right)$$
13	10 11 12	syl2anc	$$⊢A\in ℂ\to \sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-5A+12\mathrm{\pi }\right)=\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-5A\right)$$
14	7 5 8	subdid	$$⊢A\in ℂ\to 5\left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)=5\left(\frac{\mathrm{\pi }}{2}\right)-5A$$
15	4	mullidi	$$⊢1\left(\frac{\mathrm{\pi }}{2}\right)=\frac{\mathrm{\pi }}{2}$$
16	15	eqcomi	$$⊢\frac{\mathrm{\pi }}{2}=1\left(\frac{\mathrm{\pi }}{2}\right)$$
17	16	a1i	$$⊢A\in ℂ\to \frac{\mathrm{\pi }}{2}=1\left(\frac{\mathrm{\pi }}{2}\right)$$
18		2picn	$$⊢2\mathrm{\pi }\in ℂ$$
19	18	mullidi	$$⊢12\mathrm{\pi }=2\mathrm{\pi }$$
20	1 2 3	divcan2i	$$⊢2\left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{\pi }$$
21	20	eqcomi	$$⊢\mathrm{\pi }=2\left(\frac{\mathrm{\pi }}{2}\right)$$
22	21	oveq2i	$$⊢2\mathrm{\pi }=22\left(\frac{\mathrm{\pi }}{2}\right)$$
23	2 2 4	mulassi	$$⊢2\cdot 2\left(\frac{\mathrm{\pi }}{2}\right)=22\left(\frac{\mathrm{\pi }}{2}\right)$$
24		2t2e4	$$⊢2\cdot 2=4$$
25	24	oveq1i	$$⊢2\cdot 2\left(\frac{\mathrm{\pi }}{2}\right)=4\left(\frac{\mathrm{\pi }}{2}\right)$$
26	23 25	eqtr3i	$$⊢22\left(\frac{\mathrm{\pi }}{2}\right)=4\left(\frac{\mathrm{\pi }}{2}\right)$$
27	19 22 26	3eqtri	$$⊢12\mathrm{\pi }=4\left(\frac{\mathrm{\pi }}{2}\right)$$
28	27	a1i	$$⊢A\in ℂ\to 12\mathrm{\pi }=4\left(\frac{\mathrm{\pi }}{2}\right)$$
29	17 28	oveq12d	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)+12\mathrm{\pi }=1\left(\frac{\mathrm{\pi }}{2}\right)+4\left(\frac{\mathrm{\pi }}{2}\right)$$
30		1cnd	$$⊢A\in ℂ\to 1\in ℂ$$
31		4cn	$$⊢4\in ℂ$$
32	31	a1i	$$⊢A\in ℂ\to 4\in ℂ$$
33	30 32 5	adddird	$$⊢A\in ℂ\to \left(1+4\right)\left(\frac{\mathrm{\pi }}{2}\right)=1\left(\frac{\mathrm{\pi }}{2}\right)+4\left(\frac{\mathrm{\pi }}{2}\right)$$
34		ax-1cn	$$⊢1\in ℂ$$
35		df-5	$$⊢5=4+1$$
36	31 34 35	comraddi	$$⊢5=1+4$$
37	36	eqcomi	$$⊢1+4=5$$
38	37	a1i	$$⊢A\in ℂ\to 1+4=5$$
39	38	oveq1d	$$⊢A\in ℂ\to \left(1+4\right)\left(\frac{\mathrm{\pi }}{2}\right)=5\left(\frac{\mathrm{\pi }}{2}\right)$$
40	29 33 39	3eqtr2d	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)+12\mathrm{\pi }=5\left(\frac{\mathrm{\pi }}{2}\right)$$
41	40	oveq1d	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)+12\mathrm{\pi }-5A=5\left(\frac{\mathrm{\pi }}{2}\right)-5A$$
42	34 18	mulcli	$$⊢12\mathrm{\pi }\in ℂ$$
43	42	a1i	$$⊢A\in ℂ\to 12\mathrm{\pi }\in ℂ$$
44	5 43 9	addsubd	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)+12\mathrm{\pi }-5A=\left(\frac{\mathrm{\pi }}{2}\right)-5A+12\mathrm{\pi }$$
45	14 41 44	3eqtr2rd	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)-5A+12\mathrm{\pi }=5\left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)$$
46	45	fveq2d	$$⊢A\in ℂ\to \sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-5A+12\mathrm{\pi }\right)=\sin 5\left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)$$
47		sinhalfpim	$$⊢5A\in ℂ\to \sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-5A\right)=\cos 5A$$
48	9 47	syl	$$⊢A\in ℂ\to \sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-5A\right)=\cos 5A$$
49	13 46 48	3eqtr3rd	$$⊢A\in ℂ\to \cos 5A=\sin 5\left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)$$
50	5 8	subcld	$$⊢A\in ℂ\to \left(\frac{\mathrm{\pi }}{2}\right)-A\in ℂ$$
51		sin5t	$$⊢\left(\frac{\mathrm{\pi }}{2}\right)-A\in ℂ\to \sin 5\left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)=16{\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^5-20{\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^3+5\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)$$
52	50 51	syl	$$⊢A\in ℂ\to \sin 5\left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)=16{\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^5-20{\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^3+5\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)$$
53		sinhalfpim	$$⊢A\in ℂ\to \sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)=\cos A$$
54	53	oveq1d	$$⊢A\in ℂ\to {\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^5={\cos A}^5$$
55	54	oveq2d	$$⊢A\in ℂ\to 16{\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^5=16{\cos A}^5$$
56	53	oveq1d	$$⊢A\in ℂ\to {\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^3={\cos A}^3$$
57	56	oveq2d	$$⊢A\in ℂ\to 20{\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^3=20{\cos A}^3$$
58	55 57	oveq12d	$$⊢A\in ℂ\to 16{\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^5-20{\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^3=16{\cos A}^5-20{\cos A}^3$$
59	53	oveq2d	$$⊢A\in ℂ\to 5\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)=5\cos A$$
60	58 59	oveq12d	$$⊢A\in ℂ\to 16{\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^5-20{\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)}^3+5\sin \left(\left(\frac{\mathrm{\pi }}{2}\right)-A\right)=16{\cos A}^5-20{\cos A}^3+5\cos A$$
61	49 52 60	3eqtrd	$$⊢A\in ℂ\to \cos 5A=16{\cos A}^5-20{\cos A}^3+5\cos A$$