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 
|- F = ( 2 x. ( cos ` ( _pi / 5 ) ) )
Assertion goldratmolem2 
|- -u 1 = ( ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) + ( 5 x. ( F / 2 ) ) )

Proof

Step Hyp Ref Expression
1 goldra.val 
 |-  F = ( 2 x. ( cos ` ( _pi / 5 ) ) )
2 1 goldracos5teq 
 |-  ( cos ` _pi ) = ( ( ( ; 1 6 x. ( ( F / 2 ) ^ 5 ) ) - ( ; 2 0 x. ( ( F / 2 ) ^ 3 ) ) ) + ( 5 x. ( F / 2 ) ) )
3 cospi 
 |-  ( cos ` _pi ) = -u 1
4 1 goldrarr 
 |-  F e. RR
5 4 recni 
 |-  F e. CC
6 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
7 5nn0 
 |-  5 e. NN0
8 expdiv 
 |-  ( ( F e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ 5 e. NN0 ) -> ( ( F / 2 ) ^ 5 ) = ( ( F ^ 5 ) / ( 2 ^ 5 ) ) )
9 5 6 7 8 mp3an 
 |-  ( ( F / 2 ) ^ 5 ) = ( ( F ^ 5 ) / ( 2 ^ 5 ) )
10 9 oveq2i 
 |-  ( ; 1 6 x. ( ( F / 2 ) ^ 5 ) ) = ( ; 1 6 x. ( ( F ^ 5 ) / ( 2 ^ 5 ) ) )
11 expcl 
 |-  ( ( F e. CC /\ 5 e. NN0 ) -> ( F ^ 5 ) e. CC )
12 5 7 11 mp2an 
 |-  ( F ^ 5 ) e. CC
13 2cn 
 |-  2 e. CC
14 expcl 
 |-  ( ( 2 e. CC /\ 5 e. NN0 ) -> ( 2 ^ 5 ) e. CC )
15 13 7 14 mp2an 
 |-  ( 2 ^ 5 ) e. CC
16 2ne0 
 |-  2 =/= 0
17 5nn 
 |-  5 e. NN
18 17 nnzi 
 |-  5 e. ZZ
19 expne0i 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 5 e. ZZ ) -> ( 2 ^ 5 ) =/= 0 )
20 13 16 18 19 mp3an 
 |-  ( 2 ^ 5 ) =/= 0
21 15 20 pm3.2i 
 |-  ( ( 2 ^ 5 ) e. CC /\ ( 2 ^ 5 ) =/= 0 )
22 16nn0 
 |-  ; 1 6 e. NN0
23 22 nn0cni 
 |-  ; 1 6 e. CC
24 1nn0 
 |-  1 e. NN0
25 6nn 
 |-  6 e. NN
26 24 25 decnncl 
 |-  ; 1 6 e. NN
27 26 nnne0i 
 |-  ; 1 6 =/= 0
28 23 27 pm3.2i 
 |-  ( ; 1 6 e. CC /\ ; 1 6 =/= 0 )
29 divdiv2 
 |-  ( ( ( F ^ 5 ) e. CC /\ ( ( 2 ^ 5 ) e. CC /\ ( 2 ^ 5 ) =/= 0 ) /\ ( ; 1 6 e. CC /\ ; 1 6 =/= 0 ) ) -> ( ( F ^ 5 ) / ( ( 2 ^ 5 ) / ; 1 6 ) ) = ( ( ( F ^ 5 ) x. ; 1 6 ) / ( 2 ^ 5 ) ) )
30 12 21 28 29 mp3an 
 |-  ( ( F ^ 5 ) / ( ( 2 ^ 5 ) / ; 1 6 ) ) = ( ( ( F ^ 5 ) x. ; 1 6 ) / ( 2 ^ 5 ) )
31 12 23 mulcomi 
 |-  ( ( F ^ 5 ) x. ; 1 6 ) = ( ; 1 6 x. ( F ^ 5 ) )
32 31 oveq1i 
 |-  ( ( ( F ^ 5 ) x. ; 1 6 ) / ( 2 ^ 5 ) ) = ( ( ; 1 6 x. ( F ^ 5 ) ) / ( 2 ^ 5 ) )
33 23 12 15 20 divassi 
 |-  ( ( ; 1 6 x. ( F ^ 5 ) ) / ( 2 ^ 5 ) ) = ( ; 1 6 x. ( ( F ^ 5 ) / ( 2 ^ 5 ) ) )
34 30 32 33 3eqtrri 
 |-  ( ; 1 6 x. ( ( F ^ 5 ) / ( 2 ^ 5 ) ) ) = ( ( F ^ 5 ) / ( ( 2 ^ 5 ) / ; 1 6 ) )
35 exp1 
 |-  ( 2 e. CC -> ( 2 ^ 1 ) = 2 )
36 13 35 ax-mp 
 |-  ( 2 ^ 1 ) = 2
37 36 eqcomi 
 |-  2 = ( 2 ^ 1 )
38 4cn 
 |-  4 e. CC
39 ax-1cn 
 |-  1 e. CC
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 e. ZZ
45 18 44 pm3.2i 
 |-  ( 5 e. ZZ /\ 4 e. ZZ )
46 expsub 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( 5 e. ZZ /\ 4 e. ZZ ) ) -> ( 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 
 |-  ( ( F ^ 5 ) / ( ( 2 ^ 5 ) / ; 1 6 ) ) = ( ( F ^ 5 ) / 2 )
53 10 34 52 3eqtri 
 |-  ( ; 1 6 x. ( ( F / 2 ) ^ 5 ) ) = ( ( F ^ 5 ) / 2 )
54 3nn0 
 |-  3 e. NN0
55 expdiv 
 |-  ( ( F e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ 3 e. NN0 ) -> ( ( F / 2 ) ^ 3 ) = ( ( F ^ 3 ) / ( 2 ^ 3 ) ) )
56 5 6 54 55 mp3an 
 |-  ( ( F / 2 ) ^ 3 ) = ( ( F ^ 3 ) / ( 2 ^ 3 ) )
57 56 oveq2i 
 |-  ( ; 2 0 x. ( ( F / 2 ) ^ 3 ) ) = ( ; 2 0 x. ( ( F ^ 3 ) / ( 2 ^ 3 ) ) )
58 5t4e20 
 |-  ( 5 x. 4 ) = ; 2 0
59 58 eqcomi 
 |-  ; 2 0 = ( 5 x. 4 )
60 59 oveq1i 
 |-  ( ; 2 0 x. ( ( F ^ 3 ) / ( 2 ^ 3 ) ) ) = ( ( 5 x. 4 ) x. ( ( F ^ 3 ) / ( 2 ^ 3 ) ) )
61 5cn 
 |-  5 e. CC
62 expcl 
 |-  ( ( F e. CC /\ 3 e. NN0 ) -> ( F ^ 3 ) e. CC )
63 5 54 62 mp2an 
 |-  ( F ^ 3 ) e. CC
64 expcl 
 |-  ( ( 2 e. CC /\ 3 e. NN0 ) -> ( 2 ^ 3 ) e. CC )
65 13 54 64 mp2an 
 |-  ( 2 ^ 3 ) e. CC
66 3z 
 |-  3 e. ZZ
67 expne0i 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 3 e. ZZ ) -> ( 2 ^ 3 ) =/= 0 )
68 13 16 66 67 mp3an 
 |-  ( 2 ^ 3 ) =/= 0
69 63 65 68 divcli 
 |-  ( ( F ^ 3 ) / ( 2 ^ 3 ) ) e. CC
70 61 38 69 mulassi 
 |-  ( ( 5 x. 4 ) x. ( ( F ^ 3 ) / ( 2 ^ 3 ) ) ) = ( 5 x. ( 4 x. ( ( F ^ 3 ) / ( 2 ^ 3 ) ) ) )
71 60 70 eqtri 
 |-  ( ; 2 0 x. ( ( F ^ 3 ) / ( 2 ^ 3 ) ) ) = ( 5 x. ( 4 x. ( ( F ^ 3 ) / ( 2 ^ 3 ) ) ) )
72 65 68 pm3.2i 
 |-  ( ( 2 ^ 3 ) e. CC /\ ( 2 ^ 3 ) =/= 0 )
73 4ne0 
 |-  4 =/= 0
74 38 73 pm3.2i 
 |-  ( 4 e. CC /\ 4 =/= 0 )
75 divdiv2 
 |-  ( ( ( F ^ 3 ) e. CC /\ ( ( 2 ^ 3 ) e. CC /\ ( 2 ^ 3 ) =/= 0 ) /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( F ^ 3 ) / ( ( 2 ^ 3 ) / 4 ) ) = ( ( ( F ^ 3 ) x. 4 ) / ( 2 ^ 3 ) ) )
76 63 72 74 75 mp3an 
 |-  ( ( F ^ 3 ) / ( ( 2 ^ 3 ) / 4 ) ) = ( ( ( F ^ 3 ) x. 4 ) / ( 2 ^ 3 ) )
77 63 38 mulcomi 
 |-  ( ( F ^ 3 ) x. 4 ) = ( 4 x. ( F ^ 3 ) )
78 77 oveq1i 
 |-  ( ( ( F ^ 3 ) x. 4 ) / ( 2 ^ 3 ) ) = ( ( 4 x. ( F ^ 3 ) ) / ( 2 ^ 3 ) )
79 38 63 65 68 divassi 
 |-  ( ( 4 x. ( F ^ 3 ) ) / ( 2 ^ 3 ) ) = ( 4 x. ( ( F ^ 3 ) / ( 2 ^ 3 ) ) )
80 76 78 79 3eqtrri 
 |-  ( 4 x. ( ( F ^ 3 ) / ( 2 ^ 3 ) ) ) = ( ( F ^ 3 ) / ( ( 2 ^ 3 ) / 4 ) )
81 4t2e8 
 |-  ( 4 x. 2 ) = 8
82 cu2 
 |-  ( 2 ^ 3 ) = 8
83 82 eqcomi 
 |-  8 = ( 2 ^ 3 )
84 81 83 eqtri 
 |-  ( 4 x. 2 ) = ( 2 ^ 3 )
85 65 38 13 73 divmuli 
 |-  ( ( ( 2 ^ 3 ) / 4 ) = 2 <-> ( 4 x. 2 ) = ( 2 ^ 3 ) )
86 84 85 mpbir 
 |-  ( ( 2 ^ 3 ) / 4 ) = 2
87 86 oveq2i 
 |-  ( ( F ^ 3 ) / ( ( 2 ^ 3 ) / 4 ) ) = ( ( F ^ 3 ) / 2 )
88 80 87 eqtri 
 |-  ( 4 x. ( ( F ^ 3 ) / ( 2 ^ 3 ) ) ) = ( ( F ^ 3 ) / 2 )
89 88 oveq2i 
 |-  ( 5 x. ( 4 x. ( ( F ^ 3 ) / ( 2 ^ 3 ) ) ) ) = ( 5 x. ( ( F ^ 3 ) / 2 ) )
90 57 71 89 3eqtri 
 |-  ( ; 2 0 x. ( ( F / 2 ) ^ 3 ) ) = ( 5 x. ( ( F ^ 3 ) / 2 ) )
91 53 90 oveq12i 
 |-  ( ( ; 1 6 x. ( ( F / 2 ) ^ 5 ) ) - ( ; 2 0 x. ( ( F / 2 ) ^ 3 ) ) ) = ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) )
92 91 oveq1i 
 |-  ( ( ( ; 1 6 x. ( ( F / 2 ) ^ 5 ) ) - ( ; 2 0 x. ( ( F / 2 ) ^ 3 ) ) ) + ( 5 x. ( F / 2 ) ) ) = ( ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) + ( 5 x. ( F / 2 ) ) )
93 2 3 92 3eqtr3i 
 |-  -u 1 = ( ( ( ( F ^ 5 ) / 2 ) - ( 5 x. ( ( F ^ 3 ) / 2 ) ) ) + ( 5 x. ( F / 2 ) ) )