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 addid1i
 |-  ( 2 + 0 ) = 2
73 50 48 66 70 72 decaddi
 |-  ( ( 8 x. 9 ) + 0 ) = ; 7 2
74 ax-1cn
 |-  1 e. CC
75 67 mulid1i
 |-  ( 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 addid2i
 |-  ( 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 addid2i
 |-  ( 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 mulid2i
 |-  ( 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