Theorem goldratmolem2

Description: Lemma 2 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	goldratmolem2	$$⊢-1=\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)+5\left(\frac{F}{2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		goldra.val	$$⊢F=2\cos \left(\frac{\mathrm{\pi }}{5}\right)$$
2	1	goldracos5teq	$$⊢\cos \mathrm{\pi }=16{\left(\frac{F}{2}\right)}^5-20{\left(\frac{F}{2}\right)}^3+5\left(\frac{F}{2}\right)$$
3		cospi	$$⊢\cos \mathrm{\pi }=-1$$
4	1	goldrarr	$$⊢F\in ℝ$$
5	4	recni	$$⊢F\in ℂ$$
6		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
7		5nn0	$$⊢5\in {\mathbb{N}}_0$$
8		expdiv	$$⊢\left(F\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge 5\in {\mathbb{N}}_0\right)\to {\left(\frac{F}{2}\right)}^5=\frac{F^5}{2^5}$$
9	5 6 7 8	mp3an	$$⊢{\left(\frac{F}{2}\right)}^5=\frac{F^5}{2^5}$$
10	9	oveq2i	$$⊢16{\left(\frac{F}{2}\right)}^5=16\left(\frac{F^5}{2^5}\right)$$
11		expcl	$$⊢\left(F\in ℂ\wedge 5\in {\mathbb{N}}_0\right)\to F^5\in ℂ$$
12	5 7 11	mp2an	$$⊢F^5\in ℂ$$
13		2cn	$$⊢2\in ℂ$$
14		expcl	$$⊢\left(2\in ℂ\wedge 5\in {\mathbb{N}}_0\right)\to 2^5\in ℂ$$
15	13 7 14	mp2an	$$⊢2^5\in ℂ$$
16		2ne0	$$⊢2\ne 0$$
17		5nn	$$⊢5\in \mathbb{N}$$
18	17	nnzi	$$⊢5\in \mathbb{Z}$$
19		expne0i	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 5\in \mathbb{Z}\right)\to 2^5\ne 0$$
20	13 16 18 19	mp3an	$$⊢2^5\ne 0$$
21	15 20	pm3.2i	$$⊢\left(2^5\in ℂ\wedge 2^5\ne 0\right)$$
22		16nn0	$$⊢16\in {\mathbb{N}}_0$$
23	22	nn0cni	$$⊢16\in ℂ$$
24		1nn0	$$⊢1\in {\mathbb{N}}_0$$
25		6nn	$$⊢6\in \mathbb{N}$$
26	24 25	decnncl	$$⊢16\in \mathbb{N}$$
27	26	nnne0i	$$⊢16\ne 0$$
28	23 27	pm3.2i	$$⊢\left(16\in ℂ\wedge 16\ne 0\right)$$
29		divdiv2	$$⊢\left(F^5\in ℂ\wedge \left(2^5\in ℂ\wedge 2^5\ne 0\right)\wedge \left(16\in ℂ\wedge 16\ne 0\right)\right)\to \frac{F^5}{\frac{2^5}{16}}=\frac{F^5\cdot 16}{2^5}$$
30	12 21 28 29	mp3an	$$⊢\frac{F^5}{\frac{2^5}{16}}=\frac{F^5\cdot 16}{2^5}$$
31	12 23	mulcomi	$$⊢F^5\cdot 16=16F^5$$
32	31	oveq1i	$$⊢\frac{F^5\cdot 16}{2^5}=\frac{16F^5}{2^5}$$
33	23 12 15 20	divassi	$$⊢\frac{16F^5}{2^5}=16\left(\frac{F^5}{2^5}\right)$$
34	30 32 33	3eqtrri	$$⊢16\left(\frac{F^5}{2^5}\right)=\frac{F^5}{\frac{2^5}{16}}$$
35		exp1	$$⊢2\in ℂ\to 2^1=2$$
36	13 35	ax-mp	$$⊢2^1=2$$
37	36	eqcomi	$$⊢2=2^1$$
38		4cn	$$⊢4\in ℂ$$
39		ax-1cn	$$⊢1\in ℂ$$
40		4p1e5	$$⊢4+1=5$$
41	38 39 40	mvlladdi	$$⊢1=5-4$$
42	41	oveq2i	$$⊢2^1=2^{5-4}$$
43	37 42	eqtri	$$⊢2=2^{5-4}$$
44		4z	$$⊢4\in \mathbb{Z}$$
45	18 44	pm3.2i	$$⊢\left(5\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)$$
46		expsub	$$⊢\left(\left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(5\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\right)\to 2^{5-4}=\frac{2^5}{2^4}$$
47	6 45 46	mp2an	$$⊢2^{5-4}=\frac{2^5}{2^4}$$
48		2exp4	$$⊢2^4=16$$
49	48	oveq2i	$$⊢\frac{2^5}{2^4}=\frac{2^5}{16}$$
50	43 47 49	3eqtri	$$⊢2=\frac{2^5}{16}$$
51	50	eqcomi	$$⊢\frac{2^5}{16}=2$$
52	51	oveq2i	$$⊢\frac{F^5}{\frac{2^5}{16}}=\frac{F^5}{2}$$
53	10 34 52	3eqtri	$$⊢16{\left(\frac{F}{2}\right)}^5=\frac{F^5}{2}$$
54		3nn0	$$⊢3\in {\mathbb{N}}_0$$
55		expdiv	$$⊢\left(F\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge 3\in {\mathbb{N}}_0\right)\to {\left(\frac{F}{2}\right)}^3=\frac{F^3}{2^3}$$
56	5 6 54 55	mp3an	$$⊢{\left(\frac{F}{2}\right)}^3=\frac{F^3}{2^3}$$
57	56	oveq2i	$$⊢20{\left(\frac{F}{2}\right)}^3=20\left(\frac{F^3}{2^3}\right)$$
58		5t4e20	$$⊢5\cdot 4=20$$
59	58	eqcomi	$$⊢20=5\cdot 4$$
60	59	oveq1i	$$⊢20\left(\frac{F^3}{2^3}\right)=5\cdot 4\left(\frac{F^3}{2^3}\right)$$
61		5cn	$$⊢5\in ℂ$$
62		expcl	$$⊢\left(F\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to F^3\in ℂ$$
63	5 54 62	mp2an	$$⊢F^3\in ℂ$$
64		expcl	$$⊢\left(2\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to 2^3\in ℂ$$
65	13 54 64	mp2an	$$⊢2^3\in ℂ$$
66		3z	$$⊢3\in \mathbb{Z}$$
67		expne0i	$$⊢\left(2\in ℂ\wedge 2\ne 0\wedge 3\in \mathbb{Z}\right)\to 2^3\ne 0$$
68	13 16 66 67	mp3an	$$⊢2^3\ne 0$$
69	63 65 68	divcli	$$⊢\frac{F^3}{2^3}\in ℂ$$
70	61 38 69	mulassi	$$⊢5\cdot 4\left(\frac{F^3}{2^3}\right)=54\left(\frac{F^3}{2^3}\right)$$
71	60 70	eqtri	$$⊢20\left(\frac{F^3}{2^3}\right)=54\left(\frac{F^3}{2^3}\right)$$
72	65 68	pm3.2i	$$⊢\left(2^3\in ℂ\wedge 2^3\ne 0\right)$$
73		4ne0	$$⊢4\ne 0$$
74	38 73	pm3.2i	$$⊢\left(4\in ℂ\wedge 4\ne 0\right)$$
75		divdiv2	$$⊢\left(F^3\in ℂ\wedge \left(2^3\in ℂ\wedge 2^3\ne 0\right)\wedge \left(4\in ℂ\wedge 4\ne 0\right)\right)\to \frac{F^3}{\frac{2^3}{4}}=\frac{F^3\cdot 4}{2^3}$$
76	63 72 74 75	mp3an	$$⊢\frac{F^3}{\frac{2^3}{4}}=\frac{F^3\cdot 4}{2^3}$$
77	63 38	mulcomi	$$⊢F^3\cdot 4=4F^3$$
78	77	oveq1i	$$⊢\frac{F^3\cdot 4}{2^3}=\frac{4F^3}{2^3}$$
79	38 63 65 68	divassi	$$⊢\frac{4F^3}{2^3}=4\left(\frac{F^3}{2^3}\right)$$
80	76 78 79	3eqtrri	$$⊢4\left(\frac{F^3}{2^3}\right)=\frac{F^3}{\frac{2^3}{4}}$$
81		4t2e8	$$⊢4\cdot 2=8$$
82		cu2	$$⊢2^3=8$$
83	82	eqcomi	$$⊢8=2^3$$
84	81 83	eqtri	$$⊢4\cdot 2=2^3$$
85	65 38 13 73	divmuli	$$⊢\frac{2^3}{4}=2\leftrightarrow 4\cdot 2=2^3$$
86	84 85	mpbir	$$⊢\frac{2^3}{4}=2$$
87	86	oveq2i	$$⊢\frac{F^3}{\frac{2^3}{4}}=\frac{F^3}{2}$$
88	80 87	eqtri	$$⊢4\left(\frac{F^3}{2^3}\right)=\frac{F^3}{2}$$
89	88	oveq2i	$$⊢54\left(\frac{F^3}{2^3}\right)=5\left(\frac{F^3}{2}\right)$$
90	57 71 89	3eqtri	$$⊢20{\left(\frac{F}{2}\right)}^3=5\left(\frac{F^3}{2}\right)$$
91	53 90	oveq12i	$$⊢16{\left(\frac{F}{2}\right)}^5-20{\left(\frac{F}{2}\right)}^3=\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)$$
92	91	oveq1i	$$⊢16{\left(\frac{F}{2}\right)}^5-20{\left(\frac{F}{2}\right)}^3+5\left(\frac{F}{2}\right)=\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)+5\left(\frac{F}{2}\right)$$
93	2 3 92	3eqtr3i	$$⊢-1=\left(\frac{F^5}{2}\right)-5\left(\frac{F^3}{2}\right)+5\left(\frac{F}{2}\right)$$