Metamath Proof Explorer


Theorem aks4d1p1p2

Description: Rewrite A in more suitable form. (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses aks4d1p1p2.1 φ N
aks4d1p1p2.2 A = N log 2 B k = 1 log 2 N 2 N k 1
aks4d1p1p2.3 B = log 2 N 5
aks4d1p1p2.4 φ 3 N
Assertion aks4d1p1p2 φ A < N log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 4 2

Proof

Step Hyp Ref Expression
1 aks4d1p1p2.1 φ N
2 aks4d1p1p2.2 A = N log 2 B k = 1 log 2 N 2 N k 1
3 aks4d1p1p2.3 B = log 2 N 5
4 aks4d1p1p2.4 φ 3 N
5 1 nnred φ N
6 2re 2
7 6 a1i φ 2
8 2pos 0 < 2
9 8 a1i φ 0 < 2
10 1 nngt0d φ 0 < N
11 1red φ 1
12 1lt2 1 < 2
13 12 a1i φ 1 < 2
14 11 13 ltned φ 1 2
15 14 necomd φ 2 1
16 7 9 5 10 15 relogbcld φ log 2 N
17 5nn0 5 0
18 17 a1i φ 5 0
19 16 18 reexpcld φ log 2 N 5
20 ceilcl log 2 N 5 log 2 N 5
21 19 20 syl φ log 2 N 5
22 21 zred φ log 2 N 5
23 3 a1i φ B = log 2 N 5
24 23 eleq1d φ B log 2 N 5
25 22 24 mpbird φ B
26 0red φ 0
27 18 nn0zd φ 5
28 3re 3
29 28 a1i φ 3
30 1lt3 1 < 3
31 30 a1i φ 1 < 3
32 11 29 5 31 4 ltletrd φ 1 < N
33 5 10 elrpd φ N +
34 2rp 2 +
35 34 12 pm3.2i 2 + 1 < 2
36 35 a1i φ 2 + 1 < 2
37 logbgt0b N + 2 + 1 < 2 0 < log 2 N 1 < N
38 33 36 37 syl2anc φ 0 < log 2 N 1 < N
39 32 38 mpbird φ 0 < log 2 N
40 expgt0 log 2 N 5 0 < log 2 N 0 < log 2 N 5
41 16 27 39 40 syl3anc φ 0 < log 2 N 5
42 ceilge log 2 N 5 log 2 N 5 log 2 N 5
43 19 42 syl φ log 2 N 5 log 2 N 5
44 26 19 22 41 43 ltletrd φ 0 < log 2 N 5
45 23 breq2d φ 0 < B 0 < log 2 N 5
46 44 45 mpbird φ 0 < B
47 7 9 25 46 15 relogbcld φ log 2 B
48 47 flcld φ log 2 B
49 7re 7
50 49 a1i φ 7
51 1lt7 1 < 7
52 51 a1i φ 1 < 7
53 5 4 3lexlogpow5ineq3 φ 7 < log 2 N 5
54 11 50 19 52 53 lttrd φ 1 < log 2 N 5
55 11 19 22 54 43 ltletrd φ 1 < log 2 N 5
56 23 breq2d φ 1 < B 1 < log 2 N 5
57 55 56 mpbird φ 1 < B
58 25 46 elrpd φ B +
59 logbgt0b B + 2 + 1 < 2 0 < log 2 B 1 < B
60 58 36 59 syl2anc φ 0 < log 2 B 1 < B
61 57 60 mpbird φ 0 < log 2 B
62 26 47 61 ltled φ 0 log 2 B
63 0zd φ 0
64 flge log 2 B 0 0 log 2 B 0 log 2 B
65 47 63 64 syl2anc φ 0 log 2 B 0 log 2 B
66 62 65 mpbid φ 0 log 2 B
67 48 66 jca φ log 2 B 0 log 2 B
68 elnn0z log 2 B 0 log 2 B 0 log 2 B
69 67 68 sylibr φ log 2 B 0
70 5 69 reexpcld φ N log 2 B
71 fzfid φ 1 log 2 N 2 Fin
72 5 adantr φ k 1 log 2 N 2 N
73 elfznn k 1 log 2 N 2 k
74 73 adantl φ k 1 log 2 N 2 k
75 nnnn0 k k 0
76 74 75 syl φ k 1 log 2 N 2 k 0
77 72 76 reexpcld φ k 1 log 2 N 2 N k
78 1red φ k 1 log 2 N 2 1
79 77 78 resubcld φ k 1 log 2 N 2 N k 1
80 71 79 fprodrecl φ k = 1 log 2 N 2 N k 1
81 70 80 remulcld φ N log 2 B k = 1 log 2 N 2 N k 1
82 2 a1i φ A = N log 2 B k = 1 log 2 N 2 N k 1
83 82 eleq1d φ A N log 2 B k = 1 log 2 N 2 N k 1
84 81 83 mpbird φ A
85 1 nnnn0d φ N 0
86 85 nn0ge0d φ 0 N
87 19 11 readdcld φ log 2 N 5 + 1
88 19 ltp1d φ log 2 N 5 < log 2 N 5 + 1
89 26 19 87 41 88 lttrd φ 0 < log 2 N 5 + 1
90 7 9 87 89 15 relogbcld φ log 2 log 2 N 5 + 1
91 16 resqcld φ log 2 N 2
92 91 flcld φ log 2 N 2
93 92 zred φ log 2 N 2
94 0lt1 0 < 1
95 94 a1i φ 0 < 1
96 7 9 7 9 15 relogbcld φ log 2 2
97 96 resqcld φ log 2 2 2
98 2nn0 2 0
99 98 a1i φ 2 0
100 11 leidd φ 1 1
101 7 recnd φ 2
102 26 9 gtned φ 2 0
103 logbid1 2 2 0 2 1 log 2 2 = 1
104 101 102 15 103 syl3anc φ log 2 2 = 1
105 104 eqcomd φ 1 = log 2 2
106 100 105 breqtrd φ 1 log 2 2
107 96 99 106 expge1d φ 1 log 2 2 2
108 105 eqcomd φ log 2 2 = 1
109 108 oveq1d φ log 2 2 2 = 1 2
110 99 nn0zd φ 2
111 1exp 2 1 2 = 1
112 110 111 syl φ 1 2 = 1
113 109 112 eqtrd φ log 2 2 2 = 1
114 7 leidd φ 2 2
115 1nn0 1 0
116 6 115 nn0addge1i 2 2 + 1
117 2p1e3 2 + 1 = 3
118 116 117 breqtri 2 3
119 118 a1i φ 2 3
120 7 29 5 119 4 letrd φ 2 N
121 110 114 7 9 5 10 120 logblebd φ log 2 2 log 2 N
122 11 96 16 106 121 letrd φ 1 log 2 N
123 16 99 122 expge1d φ 1 log 2 N 2
124 113 123 eqbrtrd φ log 2 2 2 log 2 N 2
125 1z 1
126 zsqcl 1 1 2
127 125 126 ax-mp 1 2
128 127 a1i φ 1 2
129 109 eleq1d φ log 2 2 2 1 2
130 128 129 mpbird φ log 2 2 2
131 91 130 jca φ log 2 N 2 log 2 2 2
132 flge log 2 N 2 log 2 2 2 log 2 2 2 log 2 N 2 log 2 2 2 log 2 N 2
133 131 132 syl φ log 2 2 2 log 2 N 2 log 2 2 2 log 2 N 2
134 124 133 mpbid φ log 2 2 2 log 2 N 2
135 11 97 93 107 134 letrd φ 1 log 2 N 2
136 26 11 93 95 135 ltletrd φ 0 < log 2 N 2
137 92 136 jca φ log 2 N 2 0 < log 2 N 2
138 elnnz log 2 N 2 log 2 N 2 0 < log 2 N 2
139 138 bicomi log 2 N 2 0 < log 2 N 2 log 2 N 2
140 139 a1i φ log 2 N 2 0 < log 2 N 2 log 2 N 2
141 137 140 mpbid φ log 2 N 2
142 141 nnnn0d φ log 2 N 2 0
143 arisum log 2 N 2 0 k = 1 log 2 N 2 k = log 2 N 2 2 + log 2 N 2 2
144 142 143 syl φ k = 1 log 2 N 2 k = log 2 N 2 2 + log 2 N 2 2
145 74 nnred φ k 1 log 2 N 2 k
146 71 145 fsumrecl φ k = 1 log 2 N 2 k
147 144 146 eqeltrrd φ log 2 N 2 2 + log 2 N 2 2
148 90 147 readdcld φ log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 2 2
149 5 86 148 recxpcld φ N log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 2 2
150 4nn0 4 0
151 150 a1i φ 4 0
152 16 151 reexpcld φ log 2 N 4
153 152 91 readdcld φ log 2 N 4 + log 2 N 2
154 153 rehalfcld φ log 2 N 4 + log 2 N 2 2
155 90 154 readdcld φ log 2 log 2 N 5 + 1 + log 2 N 4 + log 2 N 2 2
156 5 86 155 recxpcld φ N log 2 log 2 N 5 + 1 + log 2 N 4 + log 2 N 2 2
157 reflcl log 2 B log 2 B
158 47 157 syl φ log 2 B
159 5 86 158 recxpcld φ N log 2 B
160 33 146 rpcxpcld φ N k = 1 log 2 N 2 k +
161 33 141 aks4d1p1p1 φ k = 1 log 2 N 2 N k = N k = 1 log 2 N 2 k
162 161 eleq1d φ k = 1 log 2 N 2 N k + N k = 1 log 2 N 2 k +
163 160 162 mpbird φ k = 1 log 2 N 2 N k +
164 163 rpregt0d φ k = 1 log 2 N 2 N k 0 < k = 1 log 2 N 2 N k
165 164 simpld φ k = 1 log 2 N 2 N k
166 159 165 remulcld φ N log 2 B k = 1 log 2 N 2 N k
167 5 86 90 recxpcld φ N log 2 log 2 N 5 + 1
168 167 165 remulcld φ N log 2 log 2 N 5 + 1 k = 1 log 2 N 2 N k
169 71 77 fprodrecl φ k = 1 log 2 N 2 N k
170 5 69 86 expge0d φ 0 N log 2 B
171 nfv k φ
172 0red φ k 1 log 2 N 2 0
173 1 nnge1d φ 1 N
174 173 adantr φ k 1 log 2 N 2 1 N
175 72 76 174 expge1d φ k 1 log 2 N 2 1 N k
176 77 recnd φ k 1 log 2 N 2 N k
177 176 subid1d φ k 1 log 2 N 2 N k 0 = N k
178 177 breq2d φ k 1 log 2 N 2 1 N k 0 1 N k
179 175 178 mpbird φ k 1 log 2 N 2 1 N k 0
180 78 77 172 179 lesubd φ k 1 log 2 N 2 0 N k 1
181 77 lem1d φ k 1 log 2 N 2 N k 1 N k
182 171 71 79 180 77 181 fprodle φ k = 1 log 2 N 2 N k 1 k = 1 log 2 N 2 N k
183 80 169 70 170 182 lemul2ad φ N log 2 B k = 1 log 2 N 2 N k 1 N log 2 B k = 1 log 2 N 2 N k
184 82 breq1d φ A N log 2 B k = 1 log 2 N 2 N k N log 2 B k = 1 log 2 N 2 N k 1 N log 2 B k = 1 log 2 N 2 N k
185 183 184 mpbird φ A N log 2 B k = 1 log 2 N 2 N k
186 72 recnd φ k 1 log 2 N 2 N
187 cxpexp N k 0 N k = N k
188 186 76 187 syl2anc φ k 1 log 2 N 2 N k = N k
189 188 eqcomd φ k 1 log 2 N 2 N k = N k
190 189 prodeq2dv φ k = 1 log 2 N 2 N k = k = 1 log 2 N 2 N k
191 190 oveq2d φ N log 2 B k = 1 log 2 N 2 N k = N log 2 B k = 1 log 2 N 2 N k
192 185 191 breqtrd φ A N log 2 B k = 1 log 2 N 2 N k
193 5 recnd φ N
194 cxpexp N log 2 B 0 N log 2 B = N log 2 B
195 193 69 194 syl2anc φ N log 2 B = N log 2 B
196 195 oveq1d φ N log 2 B k = 1 log 2 N 2 N k = N log 2 B k = 1 log 2 N 2 N k
197 196 eqcomd φ N log 2 B k = 1 log 2 N 2 N k = N log 2 B k = 1 log 2 N 2 N k
198 192 197 breqtrd φ A N log 2 B k = 1 log 2 N 2 N k
199 159 167 164 3jca φ N log 2 B N log 2 log 2 N 5 + 1 k = 1 log 2 N 2 N k 0 < k = 1 log 2 N 2 N k
200 1 3 4 aks4d1p1p3 φ N log 2 B < N log 2 log 2 N 5 + 1
201 ltmul1a N log 2 B N log 2 log 2 N 5 + 1 k = 1 log 2 N 2 N k 0 < k = 1 log 2 N 2 N k N log 2 B < N log 2 log 2 N 5 + 1 N log 2 B k = 1 log 2 N 2 N k < N log 2 log 2 N 5 + 1 k = 1 log 2 N 2 N k
202 199 200 201 syl2anc φ N log 2 B k = 1 log 2 N 2 N k < N log 2 log 2 N 5 + 1 k = 1 log 2 N 2 N k
203 84 166 168 198 202 lelttrd φ A < N log 2 log 2 N 5 + 1 k = 1 log 2 N 2 N k
204 161 oveq2d φ N log 2 log 2 N 5 + 1 k = 1 log 2 N 2 N k = N log 2 log 2 N 5 + 1 N k = 1 log 2 N 2 k
205 203 204 breqtrd φ A < N log 2 log 2 N 5 + 1 N k = 1 log 2 N 2 k
206 144 oveq2d φ N k = 1 log 2 N 2 k = N log 2 N 2 2 + log 2 N 2 2
207 206 oveq2d φ N log 2 log 2 N 5 + 1 N k = 1 log 2 N 2 k = N log 2 log 2 N 5 + 1 N log 2 N 2 2 + log 2 N 2 2
208 205 207 breqtrd φ A < N log 2 log 2 N 5 + 1 N log 2 N 2 2 + log 2 N 2 2
209 26 10 gtned φ N 0
210 90 recnd φ log 2 log 2 N 5 + 1
211 141 nncnd φ log 2 N 2
212 211 sqcld φ log 2 N 2 2
213 212 211 addcld φ log 2 N 2 2 + log 2 N 2
214 213 halfcld φ log 2 N 2 2 + log 2 N 2 2
215 193 209 210 214 cxpaddd φ N log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 2 2 = N log 2 log 2 N 5 + 1 N log 2 N 2 2 + log 2 N 2 2
216 215 eqcomd φ N log 2 log 2 N 5 + 1 N log 2 N 2 2 + log 2 N 2 2 = N log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 2 2
217 208 216 breqtrd φ A < N log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 2 2
218 reflcl log 2 N 2 log 2 N 2
219 91 218 syl φ log 2 N 2
220 219 resqcld φ log 2 N 2 2
221 220 219 readdcld φ log 2 N 2 2 + log 2 N 2
222 34 a1i φ 2 +
223 91 99 reexpcld φ log 2 N 2 2
224 id φ φ
225 142 nn0ge0d φ 0 log 2 N 2
226 flle log 2 N 2 log 2 N 2 log 2 N 2
227 91 226 syl φ log 2 N 2 log 2 N 2
228 219 91 99 225 227 leexp1ad φ log 2 N 2 2 log 2 N 2 2
229 224 228 syl φ log 2 N 2 2 log 2 N 2 2
230 16 recnd φ log 2 N
231 230 99 99 expmuld φ log 2 N 2 2 = log 2 N 2 2
232 231 eqcomd φ log 2 N 2 2 = log 2 N 2 2
233 2t2e4 2 2 = 4
234 233 oveq2i log 2 N 2 2 = log 2 N 4
235 234 a1i φ log 2 N 2 2 = log 2 N 4
236 232 235 eqtrd φ log 2 N 2 2 = log 2 N 4
237 223 236 eqled φ log 2 N 2 2 log 2 N 4
238 220 223 152 229 237 letrd φ log 2 N 2 2 log 2 N 4
239 220 219 152 91 238 227 le2addd φ log 2 N 2 2 + log 2 N 2 log 2 N 4 + log 2 N 2
240 221 153 222 239 lediv1dd φ log 2 N 2 2 + log 2 N 2 2 log 2 N 4 + log 2 N 2 2
241 147 154 90 240 leadd2dd φ log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 2 2 log 2 log 2 N 5 + 1 + log 2 N 4 + log 2 N 2 2
242 5 32 148 155 cxpled φ log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 2 2 log 2 log 2 N 5 + 1 + log 2 N 4 + log 2 N 2 2 N log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 2 2 N log 2 log 2 N 5 + 1 + log 2 N 4 + log 2 N 2 2
243 241 242 mpbid φ N log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 2 2 N log 2 log 2 N 5 + 1 + log 2 N 4 + log 2 N 2 2
244 84 149 156 217 243 ltletrd φ A < N log 2 log 2 N 5 + 1 + log 2 N 4 + log 2 N 2 2
245 152 recnd φ log 2 N 4
246 91 recnd φ log 2 N 2
247 245 246 101 102 divdird φ log 2 N 4 + log 2 N 2 2 = log 2 N 4 2 + log 2 N 2 2
248 247 oveq2d φ log 2 log 2 N 5 + 1 + log 2 N 4 + log 2 N 2 2 = log 2 log 2 N 5 + 1 + log 2 N 4 2 + log 2 N 2 2
249 248 oveq2d φ N log 2 log 2 N 5 + 1 + log 2 N 4 + log 2 N 2 2 = N log 2 log 2 N 5 + 1 + log 2 N 4 2 + log 2 N 2 2
250 244 249 breqtrd φ A < N log 2 log 2 N 5 + 1 + log 2 N 4 2 + log 2 N 2 2
251 245 101 102 divcld φ log 2 N 4 2
252 246 101 102 divcld φ log 2 N 2 2
253 251 252 addcomd φ log 2 N 4 2 + log 2 N 2 2 = log 2 N 2 2 + log 2 N 4 2
254 253 oveq2d φ log 2 log 2 N 5 + 1 + log 2 N 4 2 + log 2 N 2 2 = log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 4 2
255 210 252 251 addassd φ log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 4 2 = log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 4 2
256 255 eqcomd φ log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 4 2 = log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 4 2
257 254 256 eqtrd φ log 2 log 2 N 5 + 1 + log 2 N 4 2 + log 2 N 2 2 = log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 4 2
258 257 oveq2d φ N log 2 log 2 N 5 + 1 + log 2 N 4 2 + log 2 N 2 2 = N log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 4 2
259 250 258 breqtrd φ A < N log 2 log 2 N 5 + 1 + log 2 N 2 2 + log 2 N 4 2