Metamath Proof Explorer

Theorem goldratmolem3

Description: Lemma 3 for determining the value of golden ratio. (Contributed by Ender Ting, 23-Jul-2026)

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

Proof

Step Hyp Ref Expression
1 goldra.val ⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
2 1 goldratmolem2 ⊢ - 1 = ( ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) )
3 2 oveq1i ⊢ ( - 1 · 2 ) = ( ( ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) ) · 2 )
4 2cn ⊢ 2 ∈ ℂ
5 4 mulm1i ⊢ ( - 1 · 2 ) = - 2
6 1 goldrarr ⊢ 𝐹 ∈ ℝ
7 6 recni ⊢ 𝐹 ∈ ℂ
8 5nn0 ⊢ 5 ∈ ℕ0
9 expcl ⊢ ( ( 𝐹 ∈ ℂ ∧ 5 ∈ ℕ0 ) → ( 𝐹 ↑ 5 ) ∈ ℂ )
10 7 8 9 mp2an ⊢ ( 𝐹 ↑ 5 ) ∈ ℂ
11 2ne0 ⊢ 2 ≠ 0
12 10 4 11 divcli ⊢ ( ( 𝐹 ↑ 5 ) / 2 ) ∈ ℂ
13 5cn ⊢ 5 ∈ ℂ
14 3nn0 ⊢ 3 ∈ ℕ0
15 expcl ⊢ ( ( 𝐹 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝐹 ↑ 3 ) ∈ ℂ )
16 7 14 15 mp2an ⊢ ( 𝐹 ↑ 3 ) ∈ ℂ
17 16 4 11 divcli ⊢ ( ( 𝐹 ↑ 3 ) / 2 ) ∈ ℂ
18 13 17 mulcli ⊢ ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ∈ ℂ
19 12 18 subcli ⊢ ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) ∈ ℂ
20 7 4 11 divcli ⊢ ( 𝐹 / 2 ) ∈ ℂ
21 13 20 mulcli ⊢ ( 5 · ( 𝐹 / 2 ) ) ∈ ℂ
22 19 21 4 adddiri ⊢ ( ( ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) ) · 2 ) = ( ( ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) · 2 ) + ( ( 5 · ( 𝐹 / 2 ) ) · 2 ) )
23 12 18 4 subdiri ⊢ ( ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) · 2 ) = ( ( ( ( 𝐹 ↑ 5 ) / 2 ) · 2 ) − ( ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) · 2 ) )
24 10 4 11 divcan1i ⊢ ( ( ( 𝐹 ↑ 5 ) / 2 ) · 2 ) = ( 𝐹 ↑ 5 )
25 13 17 4 mulassi ⊢ ( ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) · 2 ) = ( 5 · ( ( ( 𝐹 ↑ 3 ) / 2 ) · 2 ) )
26 16 4 11 divcan1i ⊢ ( ( ( 𝐹 ↑ 3 ) / 2 ) · 2 ) = ( 𝐹 ↑ 3 )
27 26 oveq2i ⊢ ( 5 · ( ( ( 𝐹 ↑ 3 ) / 2 ) · 2 ) ) = ( 5 · ( 𝐹 ↑ 3 ) )
28 25 27 eqtri ⊢ ( ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) · 2 ) = ( 5 · ( 𝐹 ↑ 3 ) )
29 24 28 oveq12i ⊢ ( ( ( ( 𝐹 ↑ 5 ) / 2 ) · 2 ) − ( ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) · 2 ) ) = ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) )
30 23 29 eqtri ⊢ ( ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) · 2 ) = ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) )
31 13 20 4 mulassi ⊢ ( ( 5 · ( 𝐹 / 2 ) ) · 2 ) = ( 5 · ( ( 𝐹 / 2 ) · 2 ) )
32 7 4 11 divcan1i ⊢ ( ( 𝐹 / 2 ) · 2 ) = 𝐹
33 32 oveq2i ⊢ ( 5 · ( ( 𝐹 / 2 ) · 2 ) ) = ( 5 · 𝐹 )
34 31 33 eqtri ⊢ ( ( 5 · ( 𝐹 / 2 ) ) · 2 ) = ( 5 · 𝐹 )
35 30 34 oveq12i ⊢ ( ( ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) · 2 ) + ( ( 5 · ( 𝐹 / 2 ) ) · 2 ) ) = ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) )
36 22 35 eqtri ⊢ ( ( ( ( ( 𝐹 ↑ 5 ) / 2 ) − ( 5 · ( ( 𝐹 ↑ 3 ) / 2 ) ) ) + ( 5 · ( 𝐹 / 2 ) ) ) · 2 ) = ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) )
37 3 5 36 3eqtr3ri ⊢ ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) = - 2
38 13 16 mulcli ⊢ ( 5 · ( 𝐹 ↑ 3 ) ) ∈ ℂ
39 10 38 subcli ⊢ ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) ∈ ℂ
40 13 7 mulcli ⊢ ( 5 · 𝐹 ) ∈ ℂ
41 39 40 addcli ⊢ ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) ∈ ℂ
42 addeq0 ⊢ ( ( ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) + 2 ) = 0 ↔ ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) = - 2 ) )
43 41 4 42 mp2an ⊢ ( ( ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) + 2 ) = 0 ↔ ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) = - 2 )
44 37 43 mpbir ⊢ ( ( ( ( 𝐹 ↑ 5 ) − ( 5 · ( 𝐹 ↑ 3 ) ) ) + ( 5 · 𝐹 ) ) + 2 ) = 0