Theorem cos5teq

Description: Five-times-angle formula for cosine, substitution helper. (Contributed by Ender Ting, 9-May-2026)

	Ref	Expression
Assertion	cos5teq	$$⊢\left(A\in ℂ\wedge B=5A\wedge C=\cos A\right)\to \cos B=16C^5-20C^3+5C$$

Proof

Step	Hyp	Ref	Expression
1		simp2	$$⊢\left(A\in ℂ\wedge B=5A\wedge C=\cos A\right)\to B=5A$$
2	1	fveq2d	$$⊢\left(A\in ℂ\wedge B=5A\wedge C=\cos A\right)\to \cos B=\cos 5A$$
3		cos5t	$$⊢A\in ℂ\to \cos 5A=16{\cos A}^5-20{\cos A}^3+5\cos A$$
4	3	3ad2ant1	$$⊢\left(A\in ℂ\wedge B=5A\wedge C=\cos A\right)\to \cos 5A=16{\cos A}^5-20{\cos A}^3+5\cos A$$
5		eqcom	$$⊢C=\cos A\leftrightarrow \cos A=C$$
6	5	biimpi	$$⊢C=\cos A\to \cos A=C$$
7	6	oveq1d	$$⊢C=\cos A\to {\cos A}^5=C^5$$
8	7	oveq2d	$$⊢C=\cos A\to 16{\cos A}^5=16C^5$$
9	6	oveq1d	$$⊢C=\cos A\to {\cos A}^3=C^3$$
10	9	oveq2d	$$⊢C=\cos A\to 20{\cos A}^3=20C^3$$
11	8 10	oveq12d	$$⊢C=\cos A\to 16{\cos A}^5-20{\cos A}^3=16C^5-20C^3$$
12	6	oveq2d	$$⊢C=\cos A\to 5\cos A=5C$$
13	11 12	oveq12d	$$⊢C=\cos A\to 16{\cos A}^5-20{\cos A}^3+5\cos A=16C^5-20C^3+5C$$
14	13	3ad2ant3	$$⊢\left(A\in ℂ\wedge B=5A\wedge C=\cos A\right)\to 16{\cos A}^5-20{\cos A}^3+5\cos A=16C^5-20C^3+5C$$
15	2 4 14	3eqtrd	$$⊢\left(A\in ℂ\wedge B=5A\wedge C=\cos A\right)\to \cos B=16C^5-20C^3+5C$$