Metamath Proof Explorer

Theorem goldratval

Description: Value of the golden ratio. (Contributed by Ender Ting, 24-Jul-2026)

Ref Expression
Hypothesis goldra.val ⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
Assertion goldratval 𝐹 = ( ( 1 + ( √ ‘ 5 ) ) / 2 )

Proof

Step Hyp Ref Expression
1 goldra.val ⊢ 𝐹 = ( 2 · ( cos ‘ ( π / 5 ) ) )
2 1lt5 ⊢ 1 < 5
3 0le1 ⊢ 0 ≤ 1
4 5nn0 ⊢ 5 ∈ ℕ0
5 4 nn0ge0i ⊢ 0 ≤ 5
6 1re ⊢ 1 ∈ ℝ
7 5re ⊢ 5 ∈ ℝ
8 6 7 sqrtlti ⊢ ( ( 0 ≤ 1 ∧ 0 ≤ 5 ) → ( 1 < 5 ↔ ( √ ‘ 1 ) < ( √ ‘ 5 ) ) )
9 3 5 8 mp2an ⊢ ( 1 < 5 ↔ ( √ ‘ 1 ) < ( √ ‘ 5 ) )
10 2 9 mpbi ⊢ ( √ ‘ 1 ) < ( √ ‘ 5 )
11 negneg1e1 ⊢ - - 1 = 1
12 sqrt1 ⊢ ( √ ‘ 1 ) = 1
13 11 12 eqtr4i ⊢ - - 1 = ( √ ‘ 1 )
14 5pos ⊢ 0 < 5
15 7 14 sqrtpclii ⊢ ( √ ‘ 5 ) ∈ ℝ
16 15 recni ⊢ ( √ ‘ 5 ) ∈ ℂ
17 16 addridi ⊢ ( ( √ ‘ 5 ) + 0 ) = ( √ ‘ 5 )
18 10 13 17 3brtr4i ⊢ - - 1 < ( ( √ ‘ 5 ) + 0 )
19 neg1rr ⊢ - 1 ∈ ℝ
20 19 renegcli ⊢ - - 1 ∈ ℝ
21 0re ⊢ 0 ∈ ℝ
22 20 15 21 ltsubadd2i ⊢ ( ( - - 1 − ( √ ‘ 5 ) ) < 0 ↔ - - 1 < ( ( √ ‘ 5 ) + 0 ) )
23 18 22 mpbir ⊢ ( - - 1 − ( √ ‘ 5 ) ) < 0
24 20 15 resubcli ⊢ ( - - 1 − ( √ ‘ 5 ) ) ∈ ℝ
25 2re ⊢ 2 ∈ ℝ
26 25 6 remulcli ⊢ ( 2 · 1 ) ∈ ℝ
27 2pos ⊢ 0 < 2
28 2t1e2 ⊢ ( 2 · 1 ) = 2
29 27 28 breqtrri ⊢ 0 < ( 2 · 1 )
30 24 21 26 29 ltdiv1ii ⊢ ( ( - - 1 − ( √ ‘ 5 ) ) < 0 ↔ ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) < ( 0 / ( 2 · 1 ) ) )
31 23 30 mpbi ⊢ ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) < ( 0 / ( 2 · 1 ) )
32 26 recni ⊢ ( 2 · 1 ) ∈ ℂ
33 21 29 gtneii ⊢ ( 2 · 1 ) ≠ 0
34 32 33 div0i ⊢ ( 0 / ( 2 · 1 ) ) = 0
35 31 34 breqtri ⊢ ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) < 0
36 24 26 33 redivcli ⊢ ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) ∈ ℝ
37 36 21 ltnsymi ⊢ ( ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) < 0 → ¬ 0 < ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) )
38 35 37 ax-mp ⊢ ¬ 0 < ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) )
39 1 goldrapos ⊢ 0 < 𝐹
40 breq2 ⊢ ( 𝐹 = ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) → ( 0 < 𝐹 ↔ 0 < ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) ) )
41 39 40 mpbii ⊢ ( 𝐹 = ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) → 0 < ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) )
42 38 41 mto ⊢ ¬ 𝐹 = ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) )
43 1 goldrarr ⊢ 𝐹 ∈ ℝ
44 43 recni ⊢ 𝐹 ∈ ℂ
45 44 sqcli ⊢ ( 𝐹 ↑ 2 ) ∈ ℂ
46 ax-1cn ⊢ 1 ∈ ℂ
47 44 46 addcli ⊢ ( 𝐹 + 1 ) ∈ ℂ
48 45 47 negsubi ⊢ ( ( 𝐹 ↑ 2 ) + - ( 𝐹 + 1 ) ) = ( ( 𝐹 ↑ 2 ) − ( 𝐹 + 1 ) )
49 45 mullidi ⊢ ( 1 · ( 𝐹 ↑ 2 ) ) = ( 𝐹 ↑ 2 )
50 44 mulm1i ⊢ ( - 1 · 𝐹 ) = - 𝐹
51 50 oveq1i ⊢ ( ( - 1 · 𝐹 ) + - 1 ) = ( - 𝐹 + - 1 )
52 44 46 negdii ⊢ - ( 𝐹 + 1 ) = ( - 𝐹 + - 1 )
53 51 52 eqtr4i ⊢ ( ( - 1 · 𝐹 ) + - 1 ) = - ( 𝐹 + 1 )
54 49 53 oveq12i ⊢ ( ( 1 · ( 𝐹 ↑ 2 ) ) + ( ( - 1 · 𝐹 ) + - 1 ) ) = ( ( 𝐹 ↑ 2 ) + - ( 𝐹 + 1 ) )
55 subsub4 ⊢ ( ( ( 𝐹 ↑ 2 ) ∈ ℂ ∧ 𝐹 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) = ( ( 𝐹 ↑ 2 ) − ( 𝐹 + 1 ) ) )
56 45 44 46 55 mp3an ⊢ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) = ( ( 𝐹 ↑ 2 ) − ( 𝐹 + 1 ) )
57 48 54 56 3eqtr4ri ⊢ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) = ( ( 1 · ( 𝐹 ↑ 2 ) ) + ( ( - 1 · 𝐹 ) + - 1 ) )
58 1 goldratmolem4 ⊢ ( ( ( 𝐹 ↑ 2 ) − 𝐹 ) − 1 ) = 0
59 57 58 eqtr3i ⊢ ( ( 1 · ( 𝐹 ↑ 2 ) ) + ( ( - 1 · 𝐹 ) + - 1 ) ) = 0
60 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
61 ax-1ne0 ⊢ 1 ≠ 0
62 61 a1i ⊢ ( ⊤ → 1 ≠ 0 )
63 neg1cn ⊢ - 1 ∈ ℂ
64 63 a1i ⊢ ( ⊤ → - 1 ∈ ℂ )
65 44 a1i ⊢ ( ⊤ → 𝐹 ∈ ℂ )
66 4cn ⊢ 4 ∈ ℂ
67 46 66 subnegi ⊢ ( 1 − - 4 ) = ( 1 + 4 )
68 neg1sqe1 ⊢ ( - 1 ↑ 2 ) = 1
69 63 mullidi ⊢ ( 1 · - 1 ) = - 1
70 69 oveq2i ⊢ ( 4 · ( 1 · - 1 ) ) = ( 4 · - 1 )
71 66 46 mulneg2i ⊢ ( 4 · - 1 ) = - ( 4 · 1 )
72 66 mulridi ⊢ ( 4 · 1 ) = 4
73 72 negeqi ⊢ - ( 4 · 1 ) = - 4
74 70 71 73 3eqtri ⊢ ( 4 · ( 1 · - 1 ) ) = - 4
75 68 74 oveq12i ⊢ ( ( - 1 ↑ 2 ) − ( 4 · ( 1 · - 1 ) ) ) = ( 1 − - 4 )
76 df-5 ⊢ 5 = ( 4 + 1 )
77 66 46 76 comraddi ⊢ 5 = ( 1 + 4 )
78 67 75 77 3eqtr4ri ⊢ 5 = ( ( - 1 ↑ 2 ) − ( 4 · ( 1 · - 1 ) ) )
79 78 a1i ⊢ ( ⊤ → 5 = ( ( - 1 ↑ 2 ) − ( 4 · ( 1 · - 1 ) ) ) )
80 60 62 64 64 65 79 quad ⊢ ( ⊤ → ( ( ( 1 · ( 𝐹 ↑ 2 ) ) + ( ( - 1 · 𝐹 ) + - 1 ) ) = 0 ↔ ( 𝐹 = ( ( - - 1 + ( √ ‘ 5 ) ) / ( 2 · 1 ) ) ∨ 𝐹 = ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) ) ) )
81 80 mptru ⊢ ( ( ( 1 · ( 𝐹 ↑ 2 ) ) + ( ( - 1 · 𝐹 ) + - 1 ) ) = 0 ↔ ( 𝐹 = ( ( - - 1 + ( √ ‘ 5 ) ) / ( 2 · 1 ) ) ∨ 𝐹 = ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) ) )
82 59 81 mpbi ⊢ ( 𝐹 = ( ( - - 1 + ( √ ‘ 5 ) ) / ( 2 · 1 ) ) ∨ 𝐹 = ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) )
83 82 ori ⊢ ( ¬ 𝐹 = ( ( - - 1 + ( √ ‘ 5 ) ) / ( 2 · 1 ) ) → 𝐹 = ( ( - - 1 − ( √ ‘ 5 ) ) / ( 2 · 1 ) ) )
84 42 83 mt3 ⊢ 𝐹 = ( ( - - 1 + ( √ ‘ 5 ) ) / ( 2 · 1 ) )
85 11 oveq1i ⊢ ( - - 1 + ( √ ‘ 5 ) ) = ( 1 + ( √ ‘ 5 ) )
86 85 28 oveq12i ⊢ ( ( - - 1 + ( √ ‘ 5 ) ) / ( 2 · 1 ) ) = ( ( 1 + ( √ ‘ 5 ) ) / 2 )
87 84 86 eqtri ⊢ 𝐹 = ( ( 1 + ( √ ‘ 5 ) ) / 2 )