Metamath Proof Explorer

Theorem goldratval

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

Ref Expression
Hypothesis goldra.val 
|- F = ( 2 x. ( cos ` ( _pi / 5 ) ) )
Assertion goldratval 
|- F = ( ( 1 + ( sqrt ` 5 ) ) / 2 )

Proof

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