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