Metamath Proof Explorer

Theorem goldratmolem2

Description: Lemma 2 for determining the value of golden ratio. (Contributed by Ender Ting, 9-May-2026)

Ref Expression
Hypothesis goldra.val ⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
Assertion goldratmolem2 - 1 = ( ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) )

Proof

Step Hyp Ref Expression
1 goldra.val ⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
2 1 goldracos5teq ⊢ ( cos ‘ π ) = ( ( ( 1 6 · ( ( 𝐹 / 2 ) ↑ 5 ) ) − ( 2 0 · ( ( 𝐹 / 2 ) ↑ 3 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) )
3 cospi ⊢ ( cos ‘ π ) = - 1
4 1 goldrarr ⊢ 𝐹 ∈ ℝ
5 4 recni ⊢ 𝐹 ∈ ℂ
6 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
7 5nn0 ⊢ 5 ∈ ℕ0
8 expdiv ⊢ ( ( 𝐹 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ 5 ∈ ℕ0 ) → ( ( 𝐹 / 2 ) ↑ 5 ) = ( ( 𝐹 ↑ 5 ) / ( 2 ↑ 5 ) ) )
9 5 6 7 8 mp3an ⊢ ( ( 𝐹 / 2 ) ↑ 5 ) = ( ( 𝐹 ↑ 5 ) / ( 2 ↑ 5 ) )
10 9 oveq2i ⊢ ( 1 6 · ( ( 𝐹 / 2 ) ↑ 5 ) ) = ( 1 6 · ( ( 𝐹 ↑ 5 ) / ( 2 ↑ 5 ) ) )
11 expcl ⊢ ( ( 𝐹 ∈ ℂ ∧ 5 ∈ ℕ0 ) → ( 𝐹 ↑ 5 ) ∈ ℂ )
12 5 7 11 mp2an ⊢ ( 𝐹 ↑ 5 ) ∈ ℂ
13 2cn ⊢ 2 ∈ ℂ
14 expcl ⊢ ( ( 2 ∈ ℂ ∧ 5 ∈ ℕ0 ) → ( 2 ↑ 5 ) ∈ ℂ )
15 13 7 14 mp2an ⊢ ( 2 ↑ 5 ) ∈ ℂ
16 2ne0 ⊢ 2 ≠ 0
17 5nn ⊢ 5 ∈ ℕ
18 17 nnzi ⊢ 5 ∈ ℤ
19 expne0i ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 5 ∈ ℤ ) → ( 2 ↑ 5 ) ≠ 0 )
20 13 16 18 19 mp3an ⊢ ( 2 ↑ 5 ) ≠ 0
21 15 20 pm3.2i ⊢ ( ( 2 ↑ 5 ) ∈ ℂ ∧ ( 2 ↑ 5 ) ≠ 0 )
22 1nn0 ⊢ 1 ∈ ℕ0
23 6nn0 ⊢ 6 ∈ ℕ0
24 22 23 deccl ⊢ 1 6 ∈ ℕ0
25 24 nn0cni ⊢ 1 6 ∈ ℂ
26 6nn ⊢ 6 ∈ ℕ
27 22 26 decnncl ⊢ 1 6 ∈ ℕ
28 27 nnne0i ⊢ 1 6 ≠ 0
29 25 28 pm3.2i ⊢ ( 1 6 ∈ ℂ ∧ 1 6 ≠ 0 )
30 divdiv2 ⊢ ( ( ( 𝐹 ↑ 5 ) ∈ ℂ ∧ ( ( 2 ↑ 5 ) ∈ ℂ ∧ ( 2 ↑ 5 ) ≠ 0 ) ∧ ( 1 6 ∈ ℂ ∧ 1 6 ≠ 0 ) ) → ( ( 𝐹 ↑ 5 ) / ( ( 2 ↑ 5 ) / 1 6 ) ) = ( ( ( 𝐹 ↑ 5 ) · 1 6 ) / ( 2 ↑ 5 ) ) )
31 12 21 29 30 mp3an ⊢ ( ( 𝐹 ↑ 5 ) / ( ( 2 ↑ 5 ) / 1 6 ) ) = ( ( ( 𝐹 ↑ 5 ) · 1 6 ) / ( 2 ↑ 5 ) )
32 12 25 mulcomi ⊢ ( ( 𝐹 ↑ 5 ) · 1 6 ) = ( 1 6 · ( 𝐹 ↑ 5 ) )
33 32 oveq1i ⊢ ( ( ( 𝐹 ↑ 5 ) · 1 6 ) / ( 2 ↑ 5 ) ) = ( ( 1 6 · ( 𝐹 ↑ 5 ) ) / ( 2 ↑ 5 ) )
34 25 12 15 20 divassi ⊢ ( ( 1 6 · ( 𝐹 ↑ 5 ) ) / ( 2 ↑ 5 ) ) = ( 1 6 · ( ( 𝐹 ↑ 5 ) / ( 2 ↑ 5 ) ) )
35 31 33 34 3eqtrri ⊢ ( 1 6 · ( ( 𝐹 ↑ 5 ) / ( 2 ↑ 5 ) ) ) = ( ( 𝐹 ↑ 5 ) / ( ( 2 ↑ 5 ) / 1 6 ) )
36 exp1 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 1 ) = 2 )
37 13 36 ax-mp ⊢ ( 2 ↑ 1 ) = 2
38 37 eqcomi ⊢ 2 = ( 2 ↑ 1 )
39 4cn ⊢ 4 ∈ ℂ
40 ax-1cn ⊢ 1 ∈ ℂ
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 ∈ ℤ
46 18 45 pm3.2i ⊢ ( 5 ∈ ℤ ∧ 4 ∈ ℤ )
47 expsub ⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( 5 ∈ ℤ ∧ 4 ∈ ℤ ) ) → ( 2 ↑ ( 5 − 4 ) ) = ( ( 2 ↑ 5 ) / ( 2 ↑ 4 ) ) )
48 6 46 47 mp2an ⊢ ( 2 ↑ ( 5 − 4 ) ) = ( ( 2 ↑ 5 ) / ( 2 ↑ 4 ) )
49 2exp4 ⊢ ( 2 ↑ 4 ) = 1 6
50 49 oveq2i ⊢ ( ( 2 ↑ 5 ) / ( 2 ↑ 4 ) ) = ( ( 2 ↑ 5 ) / 1 6 )
51 44 48 50 3eqtri ⊢ 2 = ( ( 2 ↑ 5 ) / 1 6 )
52 51 eqcomi ⊢ ( ( 2 ↑ 5 ) / 1 6 ) = 2
53 52 oveq2i ⊢ ( ( 𝐹 ↑ 5 ) / ( ( 2 ↑ 5 ) / 1 6 ) ) = ( ( 𝐹 ↑ 5 ) / 2 )
54 10 35 53 3eqtri ⊢ ( 1 6 · ( ( 𝐹 / 2 ) ↑ 5 ) ) = ( ( 𝐹 ↑ 5 ) / 2 )
55 3nn0 ⊢ 3 ∈ ℕ0
56 expdiv ⊢ ( ( 𝐹 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ 3 ∈ ℕ0 ) → ( ( 𝐹 / 2 ) ↑ 3 ) = ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) )
57 5 6 55 56 mp3an ⊢ ( ( 𝐹 / 2 ) ↑ 3 ) = ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) )
58 57 oveq2i ⊢ ( 2 0 · ( ( 𝐹 / 2 ) ↑ 3 ) ) = ( 2 0 · ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) )
59 5t4e20 ⊢ ( 5 · 4 ) = 2 0
60 59 eqcomi ⊢ 2 0 = ( 5 · 4 )
61 60 oveq1i ⊢ ( 2 0 · ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) ) = ( ( 5 · 4 ) · ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) )
62 5cn ⊢ 5 ∈ ℂ
63 expcl ⊢ ( ( 𝐹 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐹 ↑ 3 ) ∈ ℂ )
64 5 55 63 mp2an ⊢ ( 𝐹 ↑ 3 ) ∈ ℂ
65 expcl ⊢ ( ( 2 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 2 ↑ 3 ) ∈ ℂ )
66 13 55 65 mp2an ⊢ ( 2 ↑ 3 ) ∈ ℂ
67 3z ⊢ 3 ∈ ℤ
68 expne0i ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 3 ∈ ℤ ) → ( 2 ↑ 3 ) ≠ 0 )
69 13 16 67 68 mp3an ⊢ ( 2 ↑ 3 ) ≠ 0
70 64 66 69 divcli ⊢ ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) ∈ ℂ
71 62 39 70 mulassi ⊢ ( ( 5 · 4 ) · ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) ) = ( 5 · ( 4 · ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) ) )
72 61 71 eqtri ⊢ ( 2 0 · ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) ) = ( 5 · ( 4 · ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) ) )
73 66 69 pm3.2i ⊢ ( ( 2 ↑ 3 ) ∈ ℂ ∧ ( 2 ↑ 3 ) ≠ 0 )
74 4ne0 ⊢ 4 ≠ 0
75 39 74 pm3.2i ⊢ ( 4 ∈ ℂ ∧ 4 ≠ 0 )
76 divdiv2 ⊢ ( ( ( 𝐹 ↑ 3 ) ∈ ℂ ∧ ( ( 2 ↑ 3 ) ∈ ℂ ∧ ( 2 ↑ 3 ) ≠ 0 ) ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( 𝐹 ↑ 3 ) / ( ( 2 ↑ 3 ) / 4 ) ) = ( ( ( 𝐹 ↑ 3 ) · 4 ) / ( 2 ↑ 3 ) ) )
77 64 73 75 76 mp3an ⊢ ( ( 𝐹 ↑ 3 ) / ( ( 2 ↑ 3 ) / 4 ) ) = ( ( ( 𝐹 ↑ 3 ) · 4 ) / ( 2 ↑ 3 ) )
78 64 39 mulcomi ⊢ ( ( 𝐹 ↑ 3 ) · 4 ) = ( 4 · ( 𝐹 ↑ 3 ) )
79 78 oveq1i ⊢ ( ( ( 𝐹 ↑ 3 ) · 4 ) / ( 2 ↑ 3 ) ) = ( ( 4 · ( 𝐹 ↑ 3 ) ) / ( 2 ↑ 3 ) )
80 39 64 66 69 divassi ⊢ ( ( 4 · ( 𝐹 ↑ 3 ) ) / ( 2 ↑ 3 ) ) = ( 4 · ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) )
81 77 79 80 3eqtrri ⊢ ( 4 · ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) ) = ( ( 𝐹 ↑ 3 ) / ( ( 2 ↑ 3 ) / 4 ) )
82 4t2e8 ⊢ ( 4 · 2 ) = 8
83 cu2 ⊢ ( 2 ↑ 3 ) = 8
84 83 eqcomi ⊢ 8 = ( 2 ↑ 3 )
85 82 84 eqtri ⊢ ( 4 · 2 ) = ( 2 ↑ 3 )
86 66 39 13 74 divmuli ⊢ ( ( ( 2 ↑ 3 ) / 4 ) = 2 ↔ ( 4 · 2 ) = ( 2 ↑ 3 ) )
87 85 86 mpbir ⊢ ( ( 2 ↑ 3 ) / 4 ) = 2
88 87 oveq2i ⊢ ( ( 𝐹 ↑ 3 ) / ( ( 2 ↑ 3 ) / 4 ) ) = ( ( 𝐹 ↑ 3 ) / 2 )
89 81 88 eqtri ⊢ ( 4 · ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) ) = ( ( 𝐹 ↑ 3 ) / 2 )
90 89 oveq2i ⊢ ( 5 · ( 4 · ( ( 𝐹 ↑ 3 ) / ( 2 ↑ 3 ) ) ) ) = ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) )
91 58 72 90 3eqtri ⊢ ( 2 0 · ( ( 𝐹 / 2 ) ↑ 3 ) ) = ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) )
92 54 91 oveq12i ⊢ ( ( 1 6 · ( ( 𝐹 / 2 ) ↑ 5 ) ) − ( 2 0 · ( ( 𝐹 / 2 ) ↑ 3 ) ) ) = ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) )
93 92 oveq1i ⊢ ( ( ( 1 6 · ( ( 𝐹 / 2 ) ↑ 5 ) ) − ( 2 0 · ( ( 𝐹 / 2 ) ↑ 3 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) ) = ( ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) )
94 2 3 93 3eqtr3i ⊢ - 1 = ( ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) )