Metamath Proof Explorer


Theorem bposlem8

Description: Lemma for bpos . Evaluate F ( 6 4 ) and show it is less than log 2 . (Contributed by Mario Carneiro, 14-Mar-2014)

Ref Expression
Hypotheses bposlem7.1 F = n 2 G n + 9 4 G n 2 + log 2 2 n
bposlem7.2 G = x + log x x
Assertion bposlem8 F 64 F 64 < log 2

Proof

Step Hyp Ref Expression
1 bposlem7.1 F = n 2 G n + 9 4 G n 2 + log 2 2 n
2 bposlem7.2 G = x + log x x
3 6nn0 6 0
4 4nn 4
5 3 4 decnncl 64
6 fveq2 n = 64 n = 64
7 8cn 8
8 7 sqvali 8 2 = 8 8
9 8t8e64 8 8 = 64
10 8 9 eqtri 8 2 = 64
11 10 fveq2i 8 2 = 64
12 0re 0
13 8re 8
14 8pos 0 < 8
15 12 13 14 ltleii 0 8
16 13 sqrtsqi 0 8 8 2 = 8
17 15 16 ax-mp 8 2 = 8
18 11 17 eqtr3i 64 = 8
19 6 18 eqtrdi n = 64 n = 8
20 19 fveq2d n = 64 G n = G 8
21 8nn 8
22 nnrp 8 8 +
23 fveq2 x = 8 log x = log 8
24 cu2 2 3 = 8
25 24 fveq2i log 2 3 = log 8
26 2rp 2 +
27 3z 3
28 relogexp 2 + 3 log 2 3 = 3 log 2
29 26 27 28 mp2an log 2 3 = 3 log 2
30 25 29 eqtr3i log 8 = 3 log 2
31 23 30 eqtrdi x = 8 log x = 3 log 2
32 id x = 8 x = 8
33 31 32 oveq12d x = 8 log x x = 3 log 2 8
34 3cn 3
35 2nn 2
36 nnrp 2 2 +
37 relogcl 2 + log 2
38 35 36 37 mp2b log 2
39 38 recni log 2
40 21 nnne0i 8 0
41 34 39 7 40 div23i 3 log 2 8 = 3 8 log 2
42 33 41 eqtrdi x = 8 log x x = 3 8 log 2
43 ovex 3 8 log 2 V
44 42 2 43 fvmpt 8 + G 8 = 3 8 log 2
45 21 22 44 mp2b G 8 = 3 8 log 2
46 20 45 eqtrdi n = 64 G n = 3 8 log 2
47 46 oveq2d n = 64 2 G n = 2 3 8 log 2
48 sqrt2re 2
49 48 recni 2
50 34 7 40 divcli 3 8
51 49 50 39 mulassi 2 3 8 log 2 = 2 3 8 log 2
52 4cn 4
53 49 52 49 mul12i 2 4 2 = 4 2 2
54 2re 2
55 0le2 0 2
56 remsqsqrt 2 0 2 2 2 = 2
57 54 55 56 mp2an 2 2 = 2
58 57 oveq2i 4 2 2 = 4 2
59 4t2e8 4 2 = 8
60 53 58 59 3eqtri 2 4 2 = 8
61 60 oveq2i 2 3 2 4 2 = 2 3 8
62 52 49 mulcli 4 2
63 nnrp 4 4 +
64 4 63 ax-mp 4 +
65 rpsqrtcl 2 + 2 +
66 35 36 65 mp2b 2 +
67 rpmulcl 4 + 2 + 4 2 +
68 64 66 67 mp2an 4 2 +
69 rpne0 4 2 + 4 2 0
70 68 69 ax-mp 4 2 0
71 rpne0 2 + 2 0
72 26 65 71 mp2b 2 0
73 divcan5 3 4 2 4 2 0 2 2 0 2 3 2 4 2 = 3 4 2
74 34 73 mp3an1 4 2 4 2 0 2 2 0 2 3 2 4 2 = 3 4 2
75 62 70 49 72 74 mp4an 2 3 2 4 2 = 3 4 2
76 4ne0 4 0
77 divdiv1 3 4 4 0 2 2 0 3 4 2 = 3 4 2
78 34 77 mp3an1 4 4 0 2 2 0 3 4 2 = 3 4 2
79 52 76 49 72 78 mp4an 3 4 2 = 3 4 2
80 75 79 eqtr4i 2 3 2 4 2 = 3 4 2
81 49 34 7 40 divassi 2 3 8 = 2 3 8
82 61 80 81 3eqtr3ri 2 3 8 = 3 4 2
83 82 oveq1i 2 3 8 log 2 = 3 4 2 log 2
84 51 83 eqtr3i 2 3 8 log 2 = 3 4 2 log 2
85 47 84 eqtrdi n = 64 2 G n = 3 4 2 log 2
86 oveq1 n = 64 n 2 = 64 2
87 df-6 6 = 5 + 1
88 87 oveq2i 2 6 = 2 5 + 1
89 2exp6 2 6 = 64
90 2cn 2
91 5nn0 5 0
92 expp1 2 5 0 2 5 + 1 = 2 5 2
93 90 91 92 mp2an 2 5 + 1 = 2 5 2
94 88 89 93 3eqtr3i 64 = 2 5 2
95 94 oveq1i 64 2 = 2 5 2 2
96 nnexpcl 2 5 0 2 5
97 35 91 96 mp2an 2 5
98 97 nncni 2 5
99 2ne0 2 0
100 98 90 99 divcan4i 2 5 2 2 = 2 5
101 95 100 eqtri 64 2 = 2 5
102 86 101 eqtrdi n = 64 n 2 = 2 5
103 102 fveq2d n = 64 G n 2 = G 2 5
104 nnrp 2 5 2 5 +
105 fveq2 x = 2 5 log x = log 2 5
106 5nn 5
107 106 nnzi 5
108 relogexp 2 + 5 log 2 5 = 5 log 2
109 26 107 108 mp2an log 2 5 = 5 log 2
110 105 109 eqtrdi x = 2 5 log x = 5 log 2
111 id x = 2 5 x = 2 5
112 110 111 oveq12d x = 2 5 log x x = 5 log 2 2 5
113 5cn 5
114 97 nnne0i 2 5 0
115 113 39 98 114 div23i 5 log 2 2 5 = 5 2 5 log 2
116 112 115 eqtrdi x = 2 5 log x x = 5 2 5 log 2
117 ovex 5 2 5 log 2 V
118 116 2 117 fvmpt 2 5 + G 2 5 = 5 2 5 log 2
119 97 104 118 mp2b G 2 5 = 5 2 5 log 2
120 103 119 eqtrdi n = 64 G n 2 = 5 2 5 log 2
121 120 oveq2d n = 64 9 4 G n 2 = 9 4 5 2 5 log 2
122 9cn 9
123 122 52 76 divcli 9 4
124 113 98 114 divcli 5 2 5
125 123 124 39 mulassi 9 4 5 2 5 log 2 = 9 4 5 2 5 log 2
126 121 125 eqtr4di n = 64 9 4 G n 2 = 9 4 5 2 5 log 2
127 85 126 oveq12d n = 64 2 G n + 9 4 G n 2 = 3 4 2 log 2 + 9 4 5 2 5 log 2
128 34 52 76 divcli 3 4
129 128 49 72 divcli 3 4 2
130 123 124 mulcli 9 4 5 2 5
131 129 130 39 adddiri 3 4 2 + 9 4 5 2 5 log 2 = 3 4 2 log 2 + 9 4 5 2 5 log 2
132 127 131 eqtr4di n = 64 2 G n + 9 4 G n 2 = 3 4 2 + 9 4 5 2 5 log 2
133 oveq2 n = 64 2 n = 2 64
134 133 fveq2d n = 64 2 n = 2 64
135 5 nnrei 64
136 5 nngt0i 0 < 64
137 12 135 136 ltleii 0 64
138 54 135 55 137 sqrtmulii 2 64 = 2 64
139 18 oveq2i 2 64 = 2 8
140 138 139 eqtri 2 64 = 2 8
141 134 140 eqtrdi n = 64 2 n = 2 8
142 141 oveq2d n = 64 log 2 2 n = log 2 2 8
143 49 7 mulcli 2 8
144 rpmulcl 2 + 8 + 2 8 +
145 66 22 144 sylancr 8 2 8 +
146 rpne0 2 8 + 2 8 0
147 21 145 146 mp2b 2 8 0
148 divrec2 log 2 2 8 2 8 0 log 2 2 8 = 1 2 8 log 2
149 39 143 147 148 mp3an log 2 2 8 = 1 2 8 log 2
150 49 7 mulcomi 2 8 = 8 2
151 150 oveq2i 1 2 8 = 1 8 2
152 recdiv2 8 8 0 2 2 0 1 8 2 = 1 8 2
153 7 40 49 72 152 mp4an 1 8 2 = 1 8 2
154 151 153 eqtr4i 1 2 8 = 1 8 2
155 154 oveq1i 1 2 8 log 2 = 1 8 2 log 2
156 149 155 eqtri log 2 2 8 = 1 8 2 log 2
157 142 156 eqtrdi n = 64 log 2 2 n = 1 8 2 log 2
158 132 157 oveq12d n = 64 2 G n + 9 4 G n 2 + log 2 2 n = 3 4 2 + 9 4 5 2 5 log 2 + 1 8 2 log 2
159 129 130 addcli 3 4 2 + 9 4 5 2 5
160 7 40 reccli 1 8
161 160 49 72 divcli 1 8 2
162 159 161 39 adddiri 3 4 2 + 9 4 5 2 5 + 1 8 2 log 2 = 3 4 2 + 9 4 5 2 5 log 2 + 1 8 2 log 2
163 158 162 eqtr4di n = 64 2 G n + 9 4 G n 2 + log 2 2 n = 3 4 2 + 9 4 5 2 5 + 1 8 2 log 2
164 ovex 3 4 2 + 9 4 5 2 5 + 1 8 2 log 2 V
165 163 1 164 fvmpt 64 F 64 = 3 4 2 + 9 4 5 2 5 + 1 8 2 log 2
166 5 165 ax-mp F 64 = 3 4 2 + 9 4 5 2 5 + 1 8 2 log 2
167 3re 3
168 4re 4
169 167 168 76 redivcli 3 4
170 169 48 72 redivcli 3 4 2
171 9re 9
172 171 168 76 redivcli 9 4
173 5re 5
174 97 nnrei 2 5
175 173 174 114 redivcli 5 2 5
176 172 175 remulcli 9 4 5 2 5
177 170 176 readdcli 3 4 2 + 9 4 5 2 5
178 13 40 rereccli 1 8
179 178 48 72 redivcli 1 8 2
180 177 179 readdcli 3 4 2 + 9 4 5 2 5 + 1 8 2
181 180 38 remulcli 3 4 2 + 9 4 5 2 5 + 1 8 2 log 2
182 166 181 eqeltri F 64
183 129 130 161 add32i 3 4 2 + 9 4 5 2 5 + 1 8 2 = 3 4 2 + 1 8 2 + 9 4 5 2 5
184 6cn 6
185 ax-1cn 1
186 184 185 7 40 divdiri 6 + 1 8 = 6 8 + 1 8
187 df-7 7 = 6 + 1
188 187 oveq1i 7 8 = 6 + 1 8
189 divcan5 3 4 4 0 2 2 0 2 3 2 4 = 3 4
190 34 189 mp3an1 4 4 0 2 2 0 2 3 2 4 = 3 4
191 52 76 90 99 190 mp4an 2 3 2 4 = 3 4
192 3t2e6 3 2 = 6
193 34 90 192 mulcomli 2 3 = 6
194 52 90 59 mulcomli 2 4 = 8
195 193 194 oveq12i 2 3 2 4 = 6 8
196 191 195 eqtr3i 3 4 = 6 8
197 196 oveq1i 3 4 + 1 8 = 6 8 + 1 8
198 186 188 197 3eqtr4ri 3 4 + 1 8 = 7 8
199 198 oveq1i 3 4 + 1 8 2 = 7 8 2
200 128 160 49 72 divdiri 3 4 + 1 8 2 = 3 4 2 + 1 8 2
201 7cn 7
202 201 7 49 40 72 divdiv32i 7 8 2 = 7 2 8
203 199 200 202 3eqtr3i 3 4 2 + 1 8 2 = 7 2 8
204 203 oveq1i 3 4 2 + 1 8 2 + 9 4 5 2 5 = 7 2 8 + 9 4 5 2 5
205 183 204 eqtri 3 4 2 + 9 4 5 2 5 + 1 8 2 = 7 2 8 + 9 4 5 2 5
206 4nn0 4 0
207 9nn0 9 0
208 0nn0 0 0
209 9lt10 9 < 10
210 4lt5 4 < 5
211 206 91 207 208 209 210 decltc 49 < 50
212 7t7e49 7 7 = 49
213 57 oveq1i 2 2 5 5 = 2 5 5
214 49 49 113 113 mul4i 2 2 5 5 = 2 5 2 5
215 5t2e10 5 2 = 10
216 113 90 215 mulcomli 2 5 = 10
217 216 oveq1i 2 5 5 = 10 5
218 90 113 113 mulassi 2 5 5 = 2 5 5
219 91 dec0u 10 5 = 50
220 217 218 219 3eqtr3i 2 5 5 = 50
221 213 214 220 3eqtr3i 2 5 2 5 = 50
222 211 212 221 3brtr4i 7 7 < 2 5 2 5
223 7re 7
224 7pos 0 < 7
225 12 223 224 ltleii 0 7
226 nnrp 5 5 +
227 106 226 ax-mp 5 +
228 rpmulcl 2 + 5 + 2 5 +
229 66 227 228 mp2an 2 5 +
230 rpge0 2 5 + 0 2 5
231 229 230 ax-mp 0 2 5
232 rpre 2 5 + 2 5
233 229 232 ax-mp 2 5
234 223 233 lt2msqi 0 7 0 2 5 7 < 2 5 7 7 < 2 5 2 5
235 225 231 234 mp2an 7 < 2 5 7 7 < 2 5 2 5
236 222 235 mpbir 7 < 2 5
237 rpgt0 2 + 0 < 2
238 26 65 237 mp2b 0 < 2
239 ltdivmul 7 5 2 0 < 2 7 2 < 5 7 < 2 5
240 223 173 239 mp3an12 2 0 < 2 7 2 < 5 7 < 2 5
241 48 238 240 mp2an 7 2 < 5 7 < 2 5
242 236 241 mpbir 7 2 < 5
243 223 48 72 redivcli 7 2
244 243 173 13 14 ltdiv1ii 7 2 < 5 7 2 8 < 5 8
245 242 244 mpbi 7 2 8 < 5 8
246 divsubdir 8 3 8 8 0 8 3 8 = 8 8 3 8
247 7 34 246 mp3an12 8 8 0 8 3 8 = 8 8 3 8
248 7 40 247 mp2an 8 3 8 = 8 8 3 8
249 5p3e8 5 + 3 = 8
250 249 oveq1i 5 + 3 - 3 = 8 3
251 113 34 pncan3oi 5 + 3 - 3 = 5
252 250 251 eqtr3i 8 3 = 5
253 252 oveq1i 8 3 8 = 5 8
254 7 40 dividi 8 8 = 1
255 254 oveq1i 8 8 3 8 = 1 3 8
256 248 253 255 3eqtr3ri 1 3 8 = 5 8
257 5lt8 5 < 8
258 13 173 remulcli 8 5
259 173 13 258 ltadd2i 5 < 8 8 5 + 5 < 8 5 + 8
260 257 259 mpbi 8 5 + 5 < 8 5 + 8
261 df-9 9 = 8 + 1
262 261 oveq1i 9 5 = 8 + 1 5
263 7 185 113 adddiri 8 + 1 5 = 8 5 + 1 5
264 113 mulid2i 1 5 = 5
265 264 oveq2i 8 5 + 1 5 = 8 5 + 5
266 262 263 265 3eqtri 9 5 = 8 5 + 5
267 87 oveq2i 8 6 = 8 5 + 1
268 7 113 185 adddii 8 5 + 1 = 8 5 + 8 1
269 7 mulid1i 8 1 = 8
270 269 oveq2i 8 5 + 8 1 = 8 5 + 8
271 267 268 270 3eqtri 8 6 = 8 5 + 8
272 260 266 271 3brtr4i 9 5 < 8 6
273 171 173 remulcli 9 5
274 6re 6
275 13 274 remulcli 8 6
276 168 174 remulcli 4 2 5
277 4 97 nnmulcli 4 2 5
278 277 nngt0i 0 < 4 2 5
279 273 275 276 278 ltdiv1ii 9 5 < 8 6 9 5 4 2 5 < 8 6 4 2 5
280 272 279 mpbi 9 5 4 2 5 < 8 6 4 2 5
281 122 52 113 98 76 114 divmuldivi 9 4 5 2 5 = 9 5 4 2 5
282 nnexpcl 2 4 0 2 4
283 35 206 282 mp2an 2 4
284 283 nncni 2 4
285 283 nnne0i 2 4 0
286 divcan5 3 8 8 0 2 4 2 4 0 2 4 3 2 4 8 = 3 8
287 34 286 mp3an1 8 8 0 2 4 2 4 0 2 4 3 2 4 8 = 3 8
288 7 40 284 285 287 mp4an 2 4 3 2 4 8 = 3 8
289 df-4 4 = 3 + 1
290 289 oveq2i 2 4 = 2 3 + 1
291 3nn0 3 0
292 expp1 2 3 0 2 3 + 1 = 2 3 2
293 90 291 292 mp2an 2 3 + 1 = 2 3 2
294 24 oveq1i 2 3 2 = 8 2
295 290 293 294 3eqtri 2 4 = 8 2
296 295 oveq1i 2 4 3 = 8 2 3
297 7 90 34 mulassi 8 2 3 = 8 2 3
298 193 oveq2i 8 2 3 = 8 6
299 296 297 298 3eqtri 2 4 3 = 8 6
300 4p3e7 4 + 3 = 7
301 5p2e7 5 + 2 = 7
302 113 90 addcomi 5 + 2 = 2 + 5
303 300 301 302 3eqtr2i 4 + 3 = 2 + 5
304 303 oveq2i 2 4 + 3 = 2 2 + 5
305 expadd 2 4 0 3 0 2 4 + 3 = 2 4 2 3
306 90 206 291 305 mp3an 2 4 + 3 = 2 4 2 3
307 2nn0 2 0
308 expadd 2 2 0 5 0 2 2 + 5 = 2 2 2 5
309 90 307 91 308 mp3an 2 2 + 5 = 2 2 2 5
310 304 306 309 3eqtr3i 2 4 2 3 = 2 2 2 5
311 24 oveq2i 2 4 2 3 = 2 4 8
312 sq2 2 2 = 4
313 312 oveq1i 2 2 2 5 = 4 2 5
314 310 311 313 3eqtr3i 2 4 8 = 4 2 5
315 299 314 oveq12i 2 4 3 2 4 8 = 8 6 4 2 5
316 288 315 eqtr3i 3 8 = 8 6 4 2 5
317 280 281 316 3brtr4i 9 4 5 2 5 < 3 8
318 167 13 40 redivcli 3 8
319 1re 1
320 ltsub2 9 4 5 2 5 3 8 1 9 4 5 2 5 < 3 8 1 3 8 < 1 9 4 5 2 5
321 176 318 319 320 mp3an 9 4 5 2 5 < 3 8 1 3 8 < 1 9 4 5 2 5
322 317 321 mpbi 1 3 8 < 1 9 4 5 2 5
323 256 322 eqbrtrri 5 8 < 1 9 4 5 2 5
324 243 13 40 redivcli 7 2 8
325 173 13 40 redivcli 5 8
326 319 176 resubcli 1 9 4 5 2 5
327 324 325 326 lttri 7 2 8 < 5 8 5 8 < 1 9 4 5 2 5 7 2 8 < 1 9 4 5 2 5
328 245 323 327 mp2an 7 2 8 < 1 9 4 5 2 5
329 324 176 319 ltaddsubi 7 2 8 + 9 4 5 2 5 < 1 7 2 8 < 1 9 4 5 2 5
330 328 329 mpbir 7 2 8 + 9 4 5 2 5 < 1
331 205 330 eqbrtri 3 4 2 + 9 4 5 2 5 + 1 8 2 < 1
332 1lt2 1 < 2
333 rplogcl 2 1 < 2 log 2 +
334 54 332 333 mp2an log 2 +
335 rpgt0 log 2 + 0 < log 2
336 334 335 ax-mp 0 < log 2
337 180 319 38 336 ltmul1ii 3 4 2 + 9 4 5 2 5 + 1 8 2 < 1 3 4 2 + 9 4 5 2 5 + 1 8 2 log 2 < 1 log 2
338 331 337 mpbi 3 4 2 + 9 4 5 2 5 + 1 8 2 log 2 < 1 log 2
339 39 mulid2i 1 log 2 = log 2
340 339 eqcomi log 2 = 1 log 2
341 338 166 340 3brtr4i F 64 < log 2
342 182 341 pm3.2i F 64 F 64 < log 2