Theorem goldratmolem4

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

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

Proof

Step	Hyp	Ref	Expression
1		goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
2	1	goldrarr	$$⊢F\in ℝ$$
3		2re	$$⊢2\in ℝ$$
4	2 3	readdcli	$$⊢F+2\in ℝ$$
5	1	goldrapos	$$⊢0<F$$
6		2pos	$$⊢0<2$$
7	2 3 5 6	addgt0ii	$$⊢0<F+2$$
8	4 7	gt0ne0ii	$$⊢F+2\ne 0$$
9	8	neii	$$⊢\neg F+2=0$$
10	2	recni	$$⊢F\in ℂ$$
11	10	goldpolyfactor	$$⊢\left(F^2-F-1\right)\left(F^2-F-1\right)\left(F+2\right)=\left(F^5-5F^3\right)+5F+2$$
12	1	goldratmolem3	$$⊢\left(F^5-5F^3\right)+5F+2=0$$
13	11 12	eqtri	$$⊢\left(F^2-F-1\right)\left(F^2-F-1\right)\left(F+2\right)=0$$
14	10	sqcli	$$⊢F^2\in ℂ$$
15	14 10	subcli	$$⊢F^2-F\in ℂ$$
16		ax-1cn	$$⊢1\in ℂ$$
17	15 16	subcli	$$⊢F^2-F-1\in ℂ$$
18	17 17	mulcli	$$⊢\left(F^2-F-1\right)\left(F^2-F-1\right)\in ℂ$$
19		2cn	$$⊢2\in ℂ$$
20	10 19	addcli	$$⊢F+2\in ℂ$$
21	18 20	mul0ori	$$⊢\left(F^2-F-1\right)\left(F^2-F-1\right)\left(F+2\right)=0\leftrightarrow \left(\left(F^2-F-1\right)\left(F^2-F-1\right)=0\vee F+2=0\right)$$
22	13 21	mpbi	$$⊢\left(\left(F^2-F-1\right)\left(F^2-F-1\right)=0\vee F+2=0\right)$$
23		orcom	$$⊢\left(\left(F^2-F-1\right)\left(F^2-F-1\right)=0\vee F+2=0\right)\leftrightarrow \left(F+2=0\vee \left(F^2-F-1\right)\left(F^2-F-1\right)=0\right)$$
24	22 23	mpbi	$$⊢\left(F+2=0\vee \left(F^2-F-1\right)\left(F^2-F-1\right)=0\right)$$
25	9 24	mtpor	$$⊢\left(F^2-F-1\right)\left(F^2-F-1\right)=0$$
26	17	msq0i	$$⊢\left(F^2-F-1\right)\left(F^2-F-1\right)=0\leftrightarrow F^2-F-1=0$$
27	25 26	mpbi	$$⊢F^2-F-1=0$$