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