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