Theorem goldracos5teq

Description: Lemma 1 for determining the value of golden ratio. (Contributed by Ender Ting, 9-May-2026)

	Ref	Expression
Hypothesis	goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
Assertion	goldracos5teq	$$⊢\cos \mathrm{\pi }=16{\left(\frac{F}{2}\right)}^5-20{\left(\frac{F}{2}\right)}^3+5\left(\frac{F}{2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
2		picn	$$⊢\mathrm{\pi }\in ℂ$$
3		5cn	$$⊢5\in ℂ$$
4		5re	$$⊢5\in ℝ$$
5		5pos	$$⊢0<5$$
6	4 5	gt0ne0ii	$$⊢5\ne 0$$
7	2 3 6	divcli	$$⊢\frac{\mathrm{\pi }}{5}\in ℂ$$
8	2 3 6	divcan2i	$$⊢5\left(\frac{\mathrm{\pi }}{5}\right)=\mathrm{\pi }$$
9	8	eqcomi	$$⊢\mathrm{\pi }=5\left(\frac{\mathrm{\pi }}{5}\right)$$
10		2cn	$$⊢2\in ℂ$$
11		coscl	$$⊢\frac{\mathrm{\pi }}{5}\in ℂ\to \cos \left(\frac{\mathrm{\pi }}{5}\right)\in ℂ$$
12	7 11	ax-mp	$$⊢\cos \left(\frac{\mathrm{\pi }}{5}\right)\in ℂ$$
13		2ne0	$$⊢2\ne 0$$
14	1	eqcomi	$$⊢2\cos \left(\frac{\mathrm{\pi }}{5}\right)=F$$
15	10 12 13 14	mvllmuli	$$⊢\cos \left(\frac{\mathrm{\pi }}{5}\right)=\frac{F}{2}$$
16	15	eqcomi	$$⊢\frac{F}{2}=\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
17		cos5teq	$$⊢\left(\frac{\mathrm{\pi }}{5}\in ℂ\wedge \mathrm{\pi }=5\left(\frac{\mathrm{\pi }}{5}\right)\wedge \frac{F}{2}=\cos \left(\frac{\mathrm{\pi }}{5}\right)\right)\to \cos \mathrm{\pi }=16{\left(\frac{F}{2}\right)}^5-20{\left(\frac{F}{2}\right)}^3+5\left(\frac{F}{2}\right)$$
18	7 9 16 17	mp3an	$$⊢\cos \mathrm{\pi }=16{\left(\frac{F}{2}\right)}^5-20{\left(\frac{F}{2}\right)}^3+5\left(\frac{F}{2}\right)$$