Theorem goldratmolem3

Description: Lemma 3 for determining the value of golden ratio. (Contributed by Ender Ting, 23-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
2	1	goldratmolem2	$$⊢-1=\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)+5\left(\frac{F}{2}\right)$$
3	2	oveq1i	$$⊢-1\cdot 2=\left(\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)+5\left(\frac{F}{2}\right)\right)\cdot 2$$
4		2cn	$$⊢2\in ℂ$$
5	4	mulm1i	$$⊢-1\cdot 2=-2$$
6	1	goldrarr	$$⊢F\in ℝ$$
7	6	recni	$$⊢F\in ℂ$$
8		5nn0	$$⊢5\in {\mathbb{N}}_0$$
9		expcl	$$⊢\left(F\in ℂ\wedge 5\in {\mathbb{N}}_0\right)\to F^5\in ℂ$$
10	7 8 9	mp2an	$$⊢F^5\in ℂ$$
11		2ne0	$$⊢2\ne 0$$
12	10 4 11	divcli	$$⊢\frac{F^5}{2}\in ℂ$$
13		5cn	$$⊢5\in ℂ$$
14		3nn0	$$⊢3\in {\mathbb{N}}_0$$
15		expcl	$$⊢\left(F\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to F^3\in ℂ$$
16	7 14 15	mp2an	$$⊢F^3\in ℂ$$
17	16 4 11	divcli	$$⊢\frac{F^3}{2}\in ℂ$$
18	13 17	mulcli	$$⊢5\left(\frac{F^3}{2}\right)\in ℂ$$
19	12 18	subcli	$$⊢\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)\in ℂ$$
20	7 4 11	divcli	$$⊢\frac{F}{2}\in ℂ$$
21	13 20	mulcli	$$⊢5\left(\frac{F}{2}\right)\in ℂ$$
22	19 21 4	adddiri	$$⊢\left(\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)+5\left(\frac{F}{2}\right)\right)\cdot 2=\left(\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)\right)\cdot 2+5\left(\frac{F}{2}\right)\cdot 2$$
23	12 18 4	subdiri	$$⊢\left(\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)\right)\cdot 2=\left(\frac{F^5}{2}\right)\cdot 2-5\left(\frac{F^3}{2}\right)\cdot 2$$
24	10 4 11	divcan1i	$$⊢\left(\frac{F^5}{2}\right)\cdot 2=F^5$$
25	13 17 4	mulassi	$$⊢5\left(\frac{F^3}{2}\right)\cdot 2=5\left(\frac{F^3}{2}\right)\cdot 2$$
26	16 4 11	divcan1i	$$⊢\left(\frac{F^3}{2}\right)\cdot 2=F^3$$
27	26	oveq2i	$$⊢5\left(\frac{F^3}{2}\right)\cdot 2=5F^3$$
28	25 27	eqtri	$$⊢5\left(\frac{F^3}{2}\right)\cdot 2=5F^3$$
29	24 28	oveq12i	$$⊢\left(\frac{F^5}{2}\right)\cdot 2-5\left(\frac{F^3}{2}\right)\cdot 2=F^5-5F^3$$
30	23 29	eqtri	$$⊢\left(\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)\right)\cdot 2=F^5-5F^3$$
31	13 20 4	mulassi	$$⊢5\left(\frac{F}{2}\right)\cdot 2=5\left(\frac{F}{2}\right)\cdot 2$$
32	7 4 11	divcan1i	$$⊢\left(\frac{F}{2}\right)\cdot 2=F$$
33	32	oveq2i	$$⊢5\left(\frac{F}{2}\right)\cdot 2=5F$$
34	31 33	eqtri	$$⊢5\left(\frac{F}{2}\right)\cdot 2=5F$$
35	30 34	oveq12i	$$⊢\left(\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)\right)\cdot 2+5\left(\frac{F}{2}\right)\cdot 2=F^5-5F^3+5F$$
36	22 35	eqtri	$$⊢\left(\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)+5\left(\frac{F}{2}\right)\right)\cdot 2=F^5-5F^3+5F$$
37	3 5 36	3eqtr3ri	$$⊢F^5-5F^3+5F=-2$$
38	13 16	mulcli	$$⊢5F^3\in ℂ$$
39	10 38	subcli	$$⊢F^5-5F^3\in ℂ$$
40	13 7	mulcli	$$⊢5F\in ℂ$$
41	39 40	addcli	$$⊢F^5-5F^3+5F\in ℂ$$
42		addeq0	$$⊢\left(F^5-5F^3+5F\in ℂ\wedge 2\in ℂ\right)\to \left(\left(F^5-5F^3\right)+5F+2=0\leftrightarrow F^5-5F^3+5F=-2\right)$$
43	41 4 42	mp2an	$$⊢\left(F^5-5F^3\right)+5F+2=0\leftrightarrow F^5-5F^3+5F=-2$$
44	37 43	mpbir	$$⊢\left(F^5-5F^3\right)+5F+2=0$$