Theorem goldratval

Description: Value of the golden ratio. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Hypothesis	goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
Assertion	goldratval	$$⊢F=\frac{1+\sqrt{5}}{2}$$

Proof

Step	Hyp	Ref	Expression
1		goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
2		1lt5	$$⊢1<5$$
3		0le1	$$⊢0\le 1$$
4		5nn0	$$⊢5\in {\mathbb{N}}_0$$
5	4	nn0ge0i	$$⊢0\le 5$$
6		1re	$$⊢1\in ℝ$$
7		5re	$$⊢5\in ℝ$$
8	6 7	sqrtlti	$$⊢\left(0\le 1\wedge 0\le 5\right)\to \left(1<5\leftrightarrow \sqrt{1}<\sqrt{5}\right)$$
9	3 5 8	mp2an	$$⊢1<5\leftrightarrow \sqrt{1}<\sqrt{5}$$
10	2 9	mpbi	$$⊢\sqrt{1}<\sqrt{5}$$
11		negneg1e1	$$⊢--1=1$$
12		sqrt1	$$⊢\sqrt{1}=1$$
13	11 12	eqtr4i	$$⊢--1=\sqrt{1}$$
14		5pos	$$⊢0<5$$
15	7 14	sqrtpclii	$$⊢\sqrt{5}\in ℝ$$
16	15	recni	$$⊢\sqrt{5}\in ℂ$$
17	16	addridi	$$⊢\sqrt{5}+0=\sqrt{5}$$
18	10 13 17	3brtr4i	$$⊢--1<\sqrt{5}+0$$
19		neg1rr	$$⊢-1\in ℝ$$
20	19	renegcli	$$⊢--1\in ℝ$$
21		0re	$$⊢0\in ℝ$$
22	20 15 21	ltsubadd2i	$$⊢--1-\sqrt{5}<0\leftrightarrow --1<\sqrt{5}+0$$
23	18 22	mpbir	$$⊢--1-\sqrt{5}<0$$
24	20 15	resubcli	$$⊢--1-\sqrt{5}\in ℝ$$
25		2re	$$⊢2\in ℝ$$
26	25 6	remulcli	$$⊢2\cdot 1\in ℝ$$
27		2pos	$$⊢0<2$$
28		2t1e2	$$⊢2\cdot 1=2$$
29	27 28	breqtrri	$$⊢0<2\cdot 1$$
30	24 21 26 29	ltdiv1ii	$$⊢--1-\sqrt{5}<0\leftrightarrow \frac{--1-\sqrt{5}}{2\cdot 1}<\frac{0}{2\cdot 1}$$
31	23 30	mpbi	$$⊢\frac{--1-\sqrt{5}}{2\cdot 1}<\frac{0}{2\cdot 1}$$
32	26	recni	$$⊢2\cdot 1\in ℂ$$
33	21 29	gtneii	$$⊢2\cdot 1\ne 0$$
34	32 33	div0i	$$⊢\frac{0}{2\cdot 1}=0$$
35	31 34	breqtri	$$⊢\frac{--1-\sqrt{5}}{2\cdot 1}<0$$
36	24 26 33	redivcli	$$⊢\frac{--1-\sqrt{5}}{2\cdot 1}\in ℝ$$
37	36 21	ltnsymi	$$⊢\frac{--1-\sqrt{5}}{2\cdot 1}<0\to \neg 0<\frac{--1-\sqrt{5}}{2\cdot 1}$$
38	35 37	ax-mp	$$⊢\neg 0<\frac{--1-\sqrt{5}}{2\cdot 1}$$
39	1	goldrapos	$$⊢0<F$$
40		breq2	$$⊢F=\frac{--1-\sqrt{5}}{2\cdot 1}\to \left(0<F\leftrightarrow 0<\frac{--1-\sqrt{5}}{2\cdot 1}\right)$$
41	39 40	mpbii	$$⊢F=\frac{--1-\sqrt{5}}{2\cdot 1}\to 0<\frac{--1-\sqrt{5}}{2\cdot 1}$$
42	38 41	mto	$$⊢\neg F=\frac{--1-\sqrt{5}}{2\cdot 1}$$
43	1	goldrarr	$$⊢F\in ℝ$$
44	43	recni	$$⊢F\in ℂ$$
45	44	sqcli	$$⊢F^2\in ℂ$$
46		ax-1cn	$$⊢1\in ℂ$$
47	44 46	addcli	$$⊢F+1\in ℂ$$
48	45 47	negsubi	$$⊢F^2+\left(-\left(F+1\right)\right)=F^2-\left(F+1\right)$$
49	45	mullidi	$$⊢1F^2=F^2$$
50	44	mulm1i	$$⊢-1F=-F$$
51	50	oveq1i	$$⊢-1F+-1=-F+-1$$
52	44 46	negdii	$$⊢-\left(F+1\right)=-F+-1$$
53	51 52	eqtr4i	$$⊢-1F+-1=-\left(F+1\right)$$
54	49 53	oveq12i	$$⊢1F^2+-1F+-1=F^2+\left(-\left(F+1\right)\right)$$
55		subsub4	$$⊢\left(F^2\in ℂ\wedge F\in ℂ\wedge 1\in ℂ\right)\to F^2-F-1=F^2-\left(F+1\right)$$
56	45 44 46 55	mp3an	$$⊢F^2-F-1=F^2-\left(F+1\right)$$
57	48 54 56	3eqtr4ri	$$⊢F^2-F-1=1F^2+-1F+-1$$
58	1	goldratmolem4	$$⊢F^2-F-1=0$$
59	57 58	eqtr3i	$$⊢1F^2+-1F+-1=0$$
60		1cnd	$$⊢\top \to 1\in ℂ$$
61		ax-1ne0	$$⊢1\ne 0$$
62	61	a1i	$$⊢\top \to 1\ne 0$$
63		neg1cn	$$⊢-1\in ℂ$$
64	63	a1i	$$⊢\top \to -1\in ℂ$$
65	44	a1i	$$⊢\top \to F\in ℂ$$
66		4cn	$$⊢4\in ℂ$$
67	46 66	subnegi	$$⊢1--4=1+4$$
68		neg1sqe1	$$⊢{\left(-1\right)}^2=1$$
69	63	mullidi	$$⊢1-1=-1$$
70	69	oveq2i	$$⊢41-1=4-1$$
71	66 46	mulneg2i	$$⊢4-1=-4\cdot 1$$
72	66	mulridi	$$⊢4\cdot 1=4$$
73	72	negeqi	$$⊢-4\cdot 1=-4$$
74	70 71 73	3eqtri	$$⊢41-1=-4$$
75	68 74	oveq12i	$$⊢{\left(-1\right)}^2-41-1=1--4$$
76		df-5	$$⊢5=4+1$$
77	66 46 76	comraddi	$$⊢5=1+4$$
78	67 75 77	3eqtr4ri	$$⊢5={\left(-1\right)}^2-41-1$$
79	78	a1i	$$⊢\top \to 5={\left(-1\right)}^2-41-1$$
80	60 62 64 64 65 79	quad	$$⊢\top \to \left(1F^2+-1F+-1=0\leftrightarrow \left(F=\frac{--1+\sqrt{5}}{2\cdot 1}\vee F=\frac{--1-\sqrt{5}}{2\cdot 1}\right)\right)$$
81	80	mptru	$$⊢1F^2+-1F+-1=0\leftrightarrow \left(F=\frac{--1+\sqrt{5}}{2\cdot 1}\vee F=\frac{--1-\sqrt{5}}{2\cdot 1}\right)$$
82	59 81	mpbi	$$⊢\left(F=\frac{--1+\sqrt{5}}{2\cdot 1}\vee F=\frac{--1-\sqrt{5}}{2\cdot 1}\right)$$
83	82	ori	$$⊢\neg F=\frac{--1+\sqrt{5}}{2\cdot 1}\to F=\frac{--1-\sqrt{5}}{2\cdot 1}$$
84	42 83	mt3	$$⊢F=\frac{--1+\sqrt{5}}{2\cdot 1}$$
85	11	oveq1i	$$⊢--1+\sqrt{5}=1+\sqrt{5}$$
86	85 28	oveq12i	$$⊢\frac{--1+\sqrt{5}}{2\cdot 1}=\frac{1+\sqrt{5}}{2}$$
87	84 86	eqtri	$$⊢F=\frac{1+\sqrt{5}}{2}$$