Metamath Proof Explorer

Theorem 3lexlogpow5ineq5

Description: Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024)

Ref Expression
Assertion 3lexlogpow5ineq5 
|- ( ( 2 logb 3 ) ^ 5 ) <_ ; 1 5

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 1 a1i 
 |-  ( T. -> 2 e. RR )
3 2pos 
 |-  0 < 2
4 3 a1i 
 |-  ( T. -> 0 < 2 )
5 3re 
 |-  3 e. RR
6 5 a1i 
 |-  ( T. -> 3 e. RR )
7 3pos 
 |-  0 < 3
8 7 a1i 
 |-  ( T. -> 0 < 3 )
9 1red 
 |-  ( T. -> 1 e. RR )
10 1lt2 
 |-  1 < 2
11 10 a1i 
 |-  ( T. -> 1 < 2 )
12 9 11 ltned 
 |-  ( T. -> 1 =/= 2 )
13 12 necomd 
 |-  ( T. -> 2 =/= 1 )
14 2 4 6 8 13 relogbcld 
 |-  ( T. -> ( 2 logb 3 ) e. RR )
15 5nn0 
 |-  5 e. NN0
16 15 a1i 
 |-  ( T. -> 5 e. NN0 )
17 14 16 reexpcld 
 |-  ( T. -> ( ( 2 logb 3 ) ^ 5 ) e. RR )
18 16 nn0red 
 |-  ( T. -> 5 e. RR )
19 8 gt0ne0d 
 |-  ( T. -> 3 =/= 0 )
20 18 6 19 redivcld 
 |-  ( T. -> ( 5 / 3 ) e. RR )
21 20 16 reexpcld 
 |-  ( T. -> ( ( 5 / 3 ) ^ 5 ) e. RR )
22 1nn0 
 |-  1 e. NN0
23 5nn 
 |-  5 e. NN
24 22 23 decnncl 
 |-  ; 1 5 e. NN
25 24 a1i 
 |-  ( T. -> ; 1 5 e. NN )
26 25 nnred 
 |-  ( T. -> ; 1 5 e. RR )
27 0red 
 |-  ( T. -> 0 e. RR )
28 6 rehalfcld 
 |-  ( T. -> ( 3 / 2 ) e. RR )
29 6 2 8 4 divgt0d 
 |-  ( T. -> 0 < ( 3 / 2 ) )
30 3lexlogpow2ineq1 
 |-  ( ( 3 / 2 ) < ( 2 logb 3 ) /\ ( 2 logb 3 ) < ( 5 / 3 ) )
31 30 simpli 
 |-  ( 3 / 2 ) < ( 2 logb 3 )
32 31 a1i 
 |-  ( T. -> ( 3 / 2 ) < ( 2 logb 3 ) )
33 27 28 14 29 32 lttrd 
 |-  ( T. -> 0 < ( 2 logb 3 ) )
34 27 14 33 ltled 
 |-  ( T. -> 0 <_ ( 2 logb 3 ) )
35 30 simpri 
 |-  ( 2 logb 3 ) < ( 5 / 3 )
36 35 a1i 
 |-  ( T. -> ( 2 logb 3 ) < ( 5 / 3 ) )
37 14 20 36 ltled 
 |-  ( T. -> ( 2 logb 3 ) <_ ( 5 / 3 ) )
38 14 20 16 34 37 leexp1ad 
 |-  ( T. -> ( ( 2 logb 3 ) ^ 5 ) <_ ( ( 5 / 3 ) ^ 5 ) )
39 df-5 
 |-  5 = ( 4 + 1 )
40 39 a1i 
 |-  ( T. -> 5 = ( 4 + 1 ) )
41 40 oveq2d 
 |-  ( T. -> ( ( 5 / 3 ) ^ 5 ) = ( ( 5 / 3 ) ^ ( 4 + 1 ) ) )
42 20 recnd 
 |-  ( T. -> ( 5 / 3 ) e. CC )
43 4nn0 
 |-  4 e. NN0
44 43 a1i 
 |-  ( T. -> 4 e. NN0 )
45 42 44 expp1d 
 |-  ( T. -> ( ( 5 / 3 ) ^ ( 4 + 1 ) ) = ( ( ( 5 / 3 ) ^ 4 ) x. ( 5 / 3 ) ) )
46 41 45 eqtrd 
 |-  ( T. -> ( ( 5 / 3 ) ^ 5 ) = ( ( ( 5 / 3 ) ^ 4 ) x. ( 5 / 3 ) ) )
47 6nn0 
 |-  6 e. NN0
48 2nn0 
 |-  2 e. NN0
49 47 48 deccl 
 |-  ; 6 2 e. NN0
50 7nn0 
 |-  7 e. NN0
51 50 48 deccl 
 |-  ; 7 2 e. NN0
52 9nn0 
 |-  9 e. NN0
53 9re 
 |-  9 e. RR
54 53 a1i 
 |-  ( T. -> 9 e. RR )
55 5lt9 
 |-  5 < 9
56 55 a1i 
 |-  ( T. -> 5 < 9 )
57 18 54 56 ltled 
 |-  ( T. -> 5 <_ 9 )
58 57 mptru 
 |-  5 <_ 9
59 2lt10 
 |-  2 < ; 1 0
60 6lt7 
 |-  6 < 7
61 47 50 48 48 59 60 decltc 
 |-  ; 6 2 < ; 7 2
62 49 51 15 52 58 61 decleh 
 |-  ; ; 6 2 5 <_ ; ; 7 2 9
63 62 a1i 
 |-  ( T. -> ; ; 6 2 5 <_ ; ; 7 2 9 )
64 8nn0 
 |-  8 e. NN0
65 eqid 
 |-  ; 8 1 = ; 8 1
66 0nn0 
 |-  0 e. NN0
67 9cn 
 |-  9 e. CC
68 8cn 
 |-  8 e. CC
69 9t8e72 
 |-  ( 9 x. 8 ) = ; 7 2
70 67 68 69 mulcomli 
 |-  ( 8 x. 9 ) = ; 7 2
71 2cn 
 |-  2 e. CC
72 71 addridi 
 |-  ( 2 + 0 ) = 2
73 50 48 66 70 72 decaddi 
 |-  ( ( 8 x. 9 ) + 0 ) = ; 7 2
74 ax-1cn 
 |-  1 e. CC
75 67 mulridi 
 |-  ( 9 x. 1 ) = 9
76 52 dec0h 
 |-  9 = ; 0 9
77 76 eqcomi 
 |-  ; 0 9 = 9
78 75 77 eqtr4i 
 |-  ( 9 x. 1 ) = ; 0 9
79 67 74 78 mulcomli 
 |-  ( 1 x. 9 ) = ; 0 9
80 52 64 22 65 52 66 73 79 decmul1c 
 |-  ( ; 8 1 x. 9 ) = ; ; 7 2 9
81 80 a1i 
 |-  ( T. -> ( ; 8 1 x. 9 ) = ; ; 7 2 9 )
82 81 eqcomd 
 |-  ( T. -> ; ; 7 2 9 = ( ; 8 1 x. 9 ) )
83 63 82 breqtrd 
 |-  ( T. -> ; ; 6 2 5 <_ ( ; 8 1 x. 9 ) )
84 eqid 
 |-  4 = 4
85 2p2e4 
 |-  ( 2 + 2 ) = 4
86 84 85 eqtr4i 
 |-  4 = ( 2 + 2 )
87 86 a1i 
 |-  ( T. -> 4 = ( 2 + 2 ) )
88 87 oveq2d 
 |-  ( T. -> ( 5 ^ 4 ) = ( 5 ^ ( 2 + 2 ) ) )
89 23 nncni 
 |-  5 e. CC
90 89 a1i 
 |-  ( T. -> 5 e. CC )
91 48 a1i 
 |-  ( T. -> 2 e. NN0 )
92 90 91 91 expaddd 
 |-  ( T. -> ( 5 ^ ( 2 + 2 ) ) = ( ( 5 ^ 2 ) x. ( 5 ^ 2 ) ) )
93 89 sqvali 
 |-  ( 5 ^ 2 ) = ( 5 x. 5 )
94 5t5e25 
 |-  ( 5 x. 5 ) = ; 2 5
95 93 94 eqtri 
 |-  ( 5 ^ 2 ) = ; 2 5
96 95 a1i 
 |-  ( T. -> ( 5 ^ 2 ) = ; 2 5 )
97 96 96 oveq12d 
 |-  ( T. -> ( ( 5 ^ 2 ) x. ( 5 ^ 2 ) ) = ( ; 2 5 x. ; 2 5 ) )
98 88 92 97 3eqtrd 
 |-  ( T. -> ( 5 ^ 4 ) = ( ; 2 5 x. ; 2 5 ) )
99 48 15 deccl 
 |-  ; 2 5 e. NN0
100 eqid 
 |-  ; 2 5 = ; 2 5
101 22 48 deccl 
 |-  ; 1 2 e. NN0
102 48 dec0h 
 |-  2 = ; 0 2
103 eqid 
 |-  ; 1 2 = ; 1 2
104 99 nn0cni 
 |-  ; 2 5 e. CC
105 104 mul02i 
 |-  ( 0 x. ; 2 5 ) = 0
106 5p1e6 
 |-  ( 5 + 1 ) = 6
107 89 74 106 addcomli 
 |-  ( 1 + 5 ) = 6
108 105 107 oveq12i 
 |-  ( ( 0 x. ; 2 5 ) + ( 1 + 5 ) ) = ( 0 + 6 )
109 6cn 
 |-  6 e. CC
110 109 addlidi 
 |-  ( 0 + 6 ) = 6
111 108 110 eqtri 
 |-  ( ( 0 x. ; 2 5 ) + ( 1 + 5 ) ) = 6
112 2t2e4 
 |-  ( 2 x. 2 ) = 4
113 0p1e1 
 |-  ( 0 + 1 ) = 1
114 112 113 oveq12i 
 |-  ( ( 2 x. 2 ) + ( 0 + 1 ) ) = ( 4 + 1 )
115 4p1e5 
 |-  ( 4 + 1 ) = 5
116 114 115 eqtri 
 |-  ( ( 2 x. 2 ) + ( 0 + 1 ) ) = 5
117 5t2e10 
 |-  ( 5 x. 2 ) = ; 1 0
118 89 71 117 mulcomli 
 |-  ( 2 x. 5 ) = ; 1 0
119 71 addlidi 
 |-  ( 0 + 2 ) = 2
120 22 66 48 118 119 decaddi 
 |-  ( ( 2 x. 5 ) + 2 ) = ; 1 2
121 48 15 66 48 100 102 48 48 22 116 120 decma2c 
 |-  ( ( 2 x. ; 2 5 ) + 2 ) = ; 5 2
122 66 48 22 48 102 103 99 48 15 111 121 decmac 
 |-  ( ( 2 x. ; 2 5 ) + ; 1 2 ) = ; 6 2
123 22 66 48 117 119 decaddi 
 |-  ( ( 5 x. 2 ) + 2 ) = ; 1 2
124 15 48 15 100 15 48 123 94 decmul2c 
 |-  ( 5 x. ; 2 5 ) = ; ; 1 2 5
125 99 48 15 100 15 101 122 124 decmul1c 
 |-  ( ; 2 5 x. ; 2 5 ) = ; ; 6 2 5
126 125 a1i 
 |-  ( T. -> ( ; 2 5 x. ; 2 5 ) = ; ; 6 2 5 )
127 98 126 eqtr2d 
 |-  ( T. -> ; ; 6 2 5 = ( 5 ^ 4 ) )
128 87 oveq2d 
 |-  ( T. -> ( 3 ^ 4 ) = ( 3 ^ ( 2 + 2 ) ) )
129 3cn 
 |-  3 e. CC
130 129 a1i 
 |-  ( T. -> 3 e. CC )
131 130 91 91 expaddd 
 |-  ( T. -> ( 3 ^ ( 2 + 2 ) ) = ( ( 3 ^ 2 ) x. ( 3 ^ 2 ) ) )
132 129 sqvali 
 |-  ( 3 ^ 2 ) = ( 3 x. 3 )
133 3t3e9 
 |-  ( 3 x. 3 ) = 9
134 132 133 eqtri 
 |-  ( 3 ^ 2 ) = 9
135 134 a1i 
 |-  ( T. -> ( 3 ^ 2 ) = 9 )
136 135 135 oveq12d 
 |-  ( T. -> ( ( 3 ^ 2 ) x. ( 3 ^ 2 ) ) = ( 9 x. 9 ) )
137 9t9e81 
 |-  ( 9 x. 9 ) = ; 8 1
138 137 a1i 
 |-  ( T. -> ( 9 x. 9 ) = ; 8 1 )
139 136 138 eqtrd 
 |-  ( T. -> ( ( 3 ^ 2 ) x. ( 3 ^ 2 ) ) = ; 8 1 )
140 128 131 139 3eqtrd 
 |-  ( T. -> ( 3 ^ 4 ) = ; 8 1 )
141 140 eqcomd 
 |-  ( T. -> ; 8 1 = ( 3 ^ 4 ) )
142 141 oveq1d 
 |-  ( T. -> ( ; 8 1 x. 9 ) = ( ( 3 ^ 4 ) x. 9 ) )
143 83 127 142 3brtr3d 
 |-  ( T. -> ( 5 ^ 4 ) <_ ( ( 3 ^ 4 ) x. 9 ) )
144 18 44 reexpcld 
 |-  ( T. -> ( 5 ^ 4 ) e. RR )
145 3rp 
 |-  3 e. RR+
146 145 a1i 
 |-  ( T. -> 3 e. RR+ )
147 4z 
 |-  4 e. ZZ
148 147 a1i 
 |-  ( T. -> 4 e. ZZ )
149 146 148 rpexpcld 
 |-  ( T. -> ( 3 ^ 4 ) e. RR+ )
150 144 54 149 ledivmuld 
 |-  ( T. -> ( ( ( 5 ^ 4 ) / ( 3 ^ 4 ) ) <_ 9 <-> ( 5 ^ 4 ) <_ ( ( 3 ^ 4 ) x. 9 ) ) )
151 143 150 mpbird 
 |-  ( T. -> ( ( 5 ^ 4 ) / ( 3 ^ 4 ) ) <_ 9 )
152 18 recnd 
 |-  ( T. -> 5 e. CC )
153 152 130 19 44 expdivd 
 |-  ( T. -> ( ( 5 / 3 ) ^ 4 ) = ( ( 5 ^ 4 ) / ( 3 ^ 4 ) ) )
154 153 eqcomd 
 |-  ( T. -> ( ( 5 ^ 4 ) / ( 3 ^ 4 ) ) = ( ( 5 / 3 ) ^ 4 ) )
155 26 recnd 
 |-  ( T. -> ; 1 5 e. CC )
156 23 nngt0i 
 |-  0 < 5
157 156 a1i 
 |-  ( T. -> 0 < 5 )
158 27 157 ltned 
 |-  ( T. -> 0 =/= 5 )
159 158 necomd 
 |-  ( T. -> 5 =/= 0 )
160 155 152 130 159 19 divdiv2d 
 |-  ( T. -> ( ; 1 5 / ( 5 / 3 ) ) = ( ( ; 1 5 x. 3 ) / 5 ) )
161 5cn 
 |-  5 e. CC
162 9t5e45 
 |-  ( 9 x. 5 ) = ; 4 5
163 67 161 162 mulcomli 
 |-  ( 5 x. 9 ) = ; 4 5
164 163 a1i 
 |-  ( T. -> ( 5 x. 9 ) = ; 4 5 )
165 3nn0 
 |-  3 e. NN0
166 eqid 
 |-  ; 1 5 = ; 1 5
167 129 mullidi 
 |-  ( 1 x. 3 ) = 3
168 167 oveq1i 
 |-  ( ( 1 x. 3 ) + 1 ) = ( 3 + 1 )
169 3p1e4 
 |-  ( 3 + 1 ) = 4
170 168 169 eqtri 
 |-  ( ( 1 x. 3 ) + 1 ) = 4
171 5t3e15 
 |-  ( 5 x. 3 ) = ; 1 5
172 165 22 15 166 15 22 170 171 decmul1c 
 |-  ( ; 1 5 x. 3 ) = ; 4 5
173 172 a1i 
 |-  ( T. -> ( ; 1 5 x. 3 ) = ; 4 5 )
174 173 eqcomd 
 |-  ( T. -> ; 4 5 = ( ; 1 5 x. 3 ) )
175 164 174 eqtrd 
 |-  ( T. -> ( 5 x. 9 ) = ( ; 1 5 x. 3 ) )
176 155 130 mulcld 
 |-  ( T. -> ( ; 1 5 x. 3 ) e. CC )
177 67 a1i 
 |-  ( T. -> 9 e. CC )
178 176 152 177 159 divmuld 
 |-  ( T. -> ( ( ( ; 1 5 x. 3 ) / 5 ) = 9 <-> ( 5 x. 9 ) = ( ; 1 5 x. 3 ) ) )
179 175 178 mpbird 
 |-  ( T. -> ( ( ; 1 5 x. 3 ) / 5 ) = 9 )
180 160 179 eqtr2d 
 |-  ( T. -> 9 = ( ; 1 5 / ( 5 / 3 ) ) )
181 151 154 180 3brtr3d 
 |-  ( T. -> ( ( 5 / 3 ) ^ 4 ) <_ ( ; 1 5 / ( 5 / 3 ) ) )
182 20 44 reexpcld 
 |-  ( T. -> ( ( 5 / 3 ) ^ 4 ) e. RR )
183 18 157 elrpd 
 |-  ( T. -> 5 e. RR+ )
184 183 146 rpdivcld 
 |-  ( T. -> ( 5 / 3 ) e. RR+ )
185 182 26 184 lemuldivd 
 |-  ( T. -> ( ( ( ( 5 / 3 ) ^ 4 ) x. ( 5 / 3 ) ) <_ ; 1 5 <-> ( ( 5 / 3 ) ^ 4 ) <_ ( ; 1 5 / ( 5 / 3 ) ) ) )
186 181 185 mpbird 
 |-  ( T. -> ( ( ( 5 / 3 ) ^ 4 ) x. ( 5 / 3 ) ) <_ ; 1 5 )
187 46 186 eqbrtrd 
 |-  ( T. -> ( ( 5 / 3 ) ^ 5 ) <_ ; 1 5 )
188 17 21 26 38 187 letrd 
 |-  ( T. -> ( ( 2 logb 3 ) ^ 5 ) <_ ; 1 5 )
189 188 mptru 
 |-  ( ( 2 logb 3 ) ^ 5 ) <_ ; 1 5