Metamath Proof Explorer


Theorem pntlemr

Description: Lemma for pntlemj . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses pntlem1.r R = a + ψ a a
pntlem1.a φ A +
pntlem1.b φ B +
pntlem1.l φ L 0 1
pntlem1.d D = A + 1
pntlem1.f F = 1 1 D L 32 B D 2
pntlem1.u φ U +
pntlem1.u2 φ U A
pntlem1.e E = U D
pntlem1.k K = e B E
pntlem1.y φ Y + 1 Y
pntlem1.x φ X + Y < X
pntlem1.c φ C +
pntlem1.w W = Y + 4 L E 2 + X K 2 4 + e 32 B U E L E 2 U 3 + C
pntlem1.z φ Z W +∞
pntlem1.m M = log X log K + 1
pntlem1.n N = log Z log K 2
pntlem1.U φ z Y +∞ R z z U
pntlem1.K φ y X +∞ z + y < z 1 + L E z < K y u z 1 + L E z R u u E
pntlem1.o O = Z K J + 1 + 1 Z K J
pntlem1.v φ V +
pntlem1.V φ K J < V 1 + L E V < K K J u V 1 + L E V R u u E
pntlem1.j φ J M ..^ N
pntlem1.i I = Z 1 + L E V + 1 Z V
Assertion pntlemr φ U E L E 8 log Z I U E log Z V Z V

Proof

Step Hyp Ref Expression
1 pntlem1.r R = a + ψ a a
2 pntlem1.a φ A +
3 pntlem1.b φ B +
4 pntlem1.l φ L 0 1
5 pntlem1.d D = A + 1
6 pntlem1.f F = 1 1 D L 32 B D 2
7 pntlem1.u φ U +
8 pntlem1.u2 φ U A
9 pntlem1.e E = U D
10 pntlem1.k K = e B E
11 pntlem1.y φ Y + 1 Y
12 pntlem1.x φ X + Y < X
13 pntlem1.c φ C +
14 pntlem1.w W = Y + 4 L E 2 + X K 2 4 + e 32 B U E L E 2 U 3 + C
15 pntlem1.z φ Z W +∞
16 pntlem1.m M = log X log K + 1
17 pntlem1.n N = log Z log K 2
18 pntlem1.U φ z Y +∞ R z z U
19 pntlem1.K φ y X +∞ z + y < z 1 + L E z < K y u z 1 + L E z R u u E
20 pntlem1.o O = Z K J + 1 + 1 Z K J
21 pntlem1.v φ V +
22 pntlem1.V φ K J < V 1 + L E V < K K J u V 1 + L E V R u u E
23 pntlem1.j φ J M ..^ N
24 pntlem1.i I = Z 1 + L E V + 1 Z V
25 1 2 3 4 5 6 pntlemd φ L + D + F +
26 25 simp1d φ L +
27 1 2 3 4 5 6 7 8 9 10 pntlemc φ E + K + E 0 1 1 < K U E +
28 27 simp1d φ E +
29 26 28 rpmulcld φ L E +
30 4re 4
31 4pos 0 < 4
32 30 31 elrpii 4 +
33 rpdivcl L E + 4 + L E 4 +
34 29 32 33 sylancl φ L E 4 +
35 34 rpred φ L E 4
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pntlemb φ Z + 1 < Z e Z Z Z Y 4 L E Z log X log K + 2 log Z log K 4 U 3 + C U E L E 2 32 B log Z
37 36 simp1d φ Z +
38 37 21 rpdivcld φ Z V +
39 38 rpred φ Z V
40 35 39 remulcld φ L E 4 Z V
41 fzfid φ Z 1 + L E V + 1 Z V Fin
42 24 41 eqeltrid φ I Fin
43 hashcl I Fin I 0
44 42 43 syl φ I 0
45 44 nn0red φ I
46 40 recnd φ L E 4 Z V
47 1rp 1 +
48 rpaddcl 1 + L E + 1 + L E +
49 47 29 48 sylancr φ 1 + L E +
50 49 21 rpmulcld φ 1 + L E V +
51 37 50 rpdivcld φ Z 1 + L E V +
52 51 rpred φ Z 1 + L E V
53 reflcl Z 1 + L E V Z 1 + L E V
54 52 53 syl φ Z 1 + L E V
55 54 recnd φ Z 1 + L E V
56 1cnd φ 1
57 46 55 56 add32d φ L E 4 Z V + Z 1 + L E V + 1 = L E 4 Z V + 1 + Z 1 + L E V
58 peano2re L E 4 Z V L E 4 Z V + 1
59 40 58 syl φ L E 4 Z V + 1
60 59 54 readdcld φ L E 4 Z V + 1 + Z 1 + L E V
61 reflcl Z V Z V
62 39 61 syl φ Z V
63 peano2re Z V Z V + 1
64 62 63 syl φ Z V + 1
65 29 rphalfcld φ L E 2 +
66 65 38 rpmulcld φ L E 2 Z V +
67 66 rpred φ L E 2 Z V
68 67 52 readdcld φ L E 2 Z V + Z 1 + L E V
69 rpdivcl 4 + L E + 4 L E +
70 32 29 69 sylancr φ 4 L E +
71 70 rpred φ 4 L E
72 37 rpsqrtcld φ Z +
73 72 rpred φ Z
74 36 simp3d φ 4 L E Z log X log K + 2 log Z log K 4 U 3 + C U E L E 2 32 B log Z
75 74 simp1d φ 4 L E Z
76 50 rpred φ 1 + L E V
77 27 simp2d φ K +
78 elfzoelz J M ..^ N J
79 23 78 syl φ J
80 79 peano2zd φ J + 1
81 77 80 rpexpcld φ K J + 1 +
82 81 rpred φ K J + 1
83 22 simplrd φ 1 + L E V < K K J
84 77 rpcnd φ K
85 77 79 rpexpcld φ K J +
86 85 rpcnd φ K J
87 84 86 mulcomd φ K K J = K J K
88 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemg φ M N M log Z log K 4 N M
89 88 simp1d φ M
90 elfzouz J M ..^ N J M
91 23 90 syl φ J M
92 eluznn M J M J
93 89 91 92 syl2anc φ J
94 93 nnnn0d φ J 0
95 84 94 expp1d φ K J + 1 = K J K
96 87 95 eqtr4d φ K K J = K J + 1
97 83 96 breqtrd φ 1 + L E V < K J + 1
98 76 82 97 ltled φ 1 + L E V K J + 1
99 fzofzp1 J M ..^ N J + 1 M N
100 23 99 syl φ J + 1 M N
101 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemh φ J + 1 M N X < K J + 1 K J + 1 Z
102 100 101 mpdan φ X < K J + 1 K J + 1 Z
103 102 simprd φ K J + 1 Z
104 76 82 73 98 103 letrd φ 1 + L E V Z
105 76 73 72 lemul2d φ 1 + L E V Z Z 1 + L E V Z Z
106 104 105 mpbid φ Z 1 + L E V Z Z
107 37 rprege0d φ Z 0 Z
108 remsqsqrt Z 0 Z Z Z = Z
109 107 108 syl φ Z Z = Z
110 106 109 breqtrd φ Z 1 + L E V Z
111 37 rpred φ Z
112 73 111 50 lemuldivd φ Z 1 + L E V Z Z Z 1 + L E V
113 110 112 mpbid φ Z Z 1 + L E V
114 21 rpcnd φ V
115 114 mulid2d φ 1 V = V
116 1red φ 1
117 49 rpred φ 1 + L E
118 1re 1
119 ltaddrp 1 L E + 1 < 1 + L E
120 118 29 119 sylancr φ 1 < 1 + L E
121 116 117 21 120 ltmul1dd φ 1 V < 1 + L E V
122 115 121 eqbrtrrd φ V < 1 + L E V
123 21 50 37 ltdiv2d φ V < 1 + L E V Z 1 + L E V < Z V
124 122 123 mpbid φ Z 1 + L E V < Z V
125 52 39 124 ltled φ Z 1 + L E V Z V
126 73 52 39 113 125 letrd φ Z Z V
127 71 73 39 75 126 letrd φ 4 L E Z V
128 71 39 39 127 leadd2dd φ Z V + 4 L E Z V + Z V
129 38 rpcnd φ Z V
130 129 2timesd φ 2 Z V = Z V + Z V
131 128 130 breqtrrd φ Z V + 4 L E 2 Z V
132 39 71 readdcld φ Z V + 4 L E
133 2re 2
134 remulcl 2 Z V 2 Z V
135 133 39 134 sylancr φ 2 Z V
136 132 135 34 lemul2d φ Z V + 4 L E 2 Z V L E 4 Z V + 4 L E L E 4 2 Z V
137 131 136 mpbid φ L E 4 Z V + 4 L E L E 4 2 Z V
138 34 rpcnd φ L E 4
139 70 rpcnd φ 4 L E
140 138 129 139 adddid φ L E 4 Z V + 4 L E = L E 4 Z V + L E 4 4 L E
141 29 rpcnne0d φ L E L E 0
142 rpcnne0 4 + 4 4 0
143 32 142 mp1i φ 4 4 0
144 divcan6 L E L E 0 4 4 0 L E 4 4 L E = 1
145 141 143 144 syl2anc φ L E 4 4 L E = 1
146 145 oveq2d φ L E 4 Z V + L E 4 4 L E = L E 4 Z V + 1
147 140 146 eqtrd φ L E 4 Z V + 4 L E = L E 4 Z V + 1
148 2cnd φ 2
149 138 148 129 mulassd φ L E 4 2 Z V = L E 4 2 Z V
150 29 rpcnd φ L E
151 2rp 2 +
152 rpcnne0 2 + 2 2 0
153 151 152 mp1i φ 2 2 0
154 divdiv1 L E 2 2 0 2 2 0 L E 2 2 = L E 2 2
155 150 153 153 154 syl3anc φ L E 2 2 = L E 2 2
156 2t2e4 2 2 = 4
157 156 oveq2i L E 2 2 = L E 4
158 155 157 eqtr2di φ L E 4 = L E 2 2
159 158 oveq1d φ L E 4 2 = L E 2 2 2
160 150 halfcld φ L E 2
161 153 simprd φ 2 0
162 160 148 161 divcan1d φ L E 2 2 2 = L E 2
163 159 162 eqtrd φ L E 4 2 = L E 2
164 163 oveq1d φ L E 4 2 Z V = L E 2 Z V
165 149 164 eqtr3d φ L E 4 2 Z V = L E 2 Z V
166 137 147 165 3brtr3d φ L E 4 Z V + 1 L E 2 Z V
167 flle Z 1 + L E V Z 1 + L E V Z 1 + L E V
168 52 167 syl φ Z 1 + L E V Z 1 + L E V
169 59 54 67 52 166 168 le2addd φ L E 4 Z V + 1 + Z 1 + L E V L E 2 Z V + Z 1 + L E V
170 65 rpred φ L E 2
171 49 rprecred φ 1 1 + L E
172 170 171 readdcld φ L E 2 + 1 1 + L E
173 29 rpred φ L E
174 28 rpred φ E
175 26 rpred φ L
176 eliooord L 0 1 0 < L L < 1
177 4 176 syl φ 0 < L L < 1
178 177 simprd φ L < 1
179 175 116 28 178 ltmul1dd φ L E < 1 E
180 28 rpcnd φ E
181 180 mulid2d φ 1 E = E
182 179 181 breqtrd φ L E < E
183 27 simp3d φ E 0 1 1 < K U E +
184 183 simp1d φ E 0 1
185 eliooord E 0 1 0 < E E < 1
186 184 185 syl φ 0 < E E < 1
187 186 simprd φ E < 1
188 173 174 116 182 187 lttrd φ L E < 1
189 173 116 116 188 ltadd2dd φ 1 + L E < 1 + 1
190 df-2 2 = 1 + 1
191 189 190 breqtrrdi φ 1 + L E < 2
192 49 rpregt0d φ 1 + L E 0 < 1 + L E
193 133 a1i φ 2
194 2pos 0 < 2
195 194 a1i φ 0 < 2
196 29 rpregt0d φ L E 0 < L E
197 ltdiv2 1 + L E 0 < 1 + L E 2 0 < 2 L E 0 < L E 1 + L E < 2 L E 2 < L E 1 + L E
198 192 193 195 196 197 syl121anc φ 1 + L E < 2 L E 2 < L E 1 + L E
199 191 198 mpbid φ L E 2 < L E 1 + L E
200 49 rpcnd φ 1 + L E
201 49 rpcnne0d φ 1 + L E 1 + L E 0
202 divsubdir 1 + L E 1 1 + L E 1 + L E 0 1 + L E - 1 1 + L E = 1 + L E 1 + L E 1 1 + L E
203 200 56 201 202 syl3anc φ 1 + L E - 1 1 + L E = 1 + L E 1 + L E 1 1 + L E
204 ax-1cn 1
205 pncan2 1 L E 1 + L E - 1 = L E
206 204 150 205 sylancr φ 1 + L E - 1 = L E
207 206 oveq1d φ 1 + L E - 1 1 + L E = L E 1 + L E
208 divid 1 + L E 1 + L E 0 1 + L E 1 + L E = 1
209 201 208 syl φ 1 + L E 1 + L E = 1
210 209 oveq1d φ 1 + L E 1 + L E 1 1 + L E = 1 1 1 + L E
211 203 207 210 3eqtr3d φ L E 1 + L E = 1 1 1 + L E
212 199 211 breqtrd φ L E 2 < 1 1 1 + L E
213 170 171 116 ltaddsubd φ L E 2 + 1 1 + L E < 1 L E 2 < 1 1 1 + L E
214 212 213 mpbird φ L E 2 + 1 1 + L E < 1
215 172 116 38 214 ltmul1dd φ L E 2 + 1 1 + L E Z V < 1 Z V
216 reccl 1 + L E 1 + L E 0 1 1 + L E
217 201 216 syl φ 1 1 + L E
218 160 217 129 adddird φ L E 2 + 1 1 + L E Z V = L E 2 Z V + 1 1 + L E Z V
219 200 114 mulcomd φ 1 + L E V = V 1 + L E
220 219 oveq2d φ Z 1 + L E V = Z V 1 + L E
221 37 rpcnd φ Z
222 21 rpcnne0d φ V V 0
223 divdiv1 Z V V 0 1 + L E 1 + L E 0 Z V 1 + L E = Z V 1 + L E
224 221 222 201 223 syl3anc φ Z V 1 + L E = Z V 1 + L E
225 49 rpne0d φ 1 + L E 0
226 129 200 225 divrec2d φ Z V 1 + L E = 1 1 + L E Z V
227 220 224 226 3eqtr2d φ Z 1 + L E V = 1 1 + L E Z V
228 227 oveq2d φ L E 2 Z V + Z 1 + L E V = L E 2 Z V + 1 1 + L E Z V
229 218 228 eqtr4d φ L E 2 + 1 1 + L E Z V = L E 2 Z V + Z 1 + L E V
230 129 mulid2d φ 1 Z V = Z V
231 215 229 230 3brtr3d φ L E 2 Z V + Z 1 + L E V < Z V
232 60 68 39 169 231 lelttrd φ L E 4 Z V + 1 + Z 1 + L E V < Z V
233 fllep1 Z V Z V Z V + 1
234 39 233 syl φ Z V Z V + 1
235 60 39 64 232 234 ltletrd φ L E 4 Z V + 1 + Z 1 + L E V < Z V + 1
236 57 235 eqbrtrd φ L E 4 Z V + Z 1 + L E V + 1 < Z V + 1
237 40 54 readdcld φ L E 4 Z V + Z 1 + L E V
238 237 62 116 ltadd1d φ L E 4 Z V + Z 1 + L E V < Z V L E 4 Z V + Z 1 + L E V + 1 < Z V + 1
239 236 238 mpbird φ L E 4 Z V + Z 1 + L E V < Z V
240 40 54 62 ltaddsubd φ L E 4 Z V + Z 1 + L E V < Z V L E 4 Z V < Z V Z 1 + L E V
241 239 240 mpbid φ L E 4 Z V < Z V Z 1 + L E V
242 39 flcld φ Z V
243 fzval3 Z V Z 1 + L E V + 1 Z V = Z 1 + L E V + 1 ..^ Z V + 1
244 242 243 syl φ Z 1 + L E V + 1 Z V = Z 1 + L E V + 1 ..^ Z V + 1
245 24 244 eqtrid φ I = Z 1 + L E V + 1 ..^ Z V + 1
246 245 fveq2d φ I = Z 1 + L E V + 1 ..^ Z V + 1
247 flword2 Z 1 + L E V Z V Z 1 + L E V Z V Z V Z 1 + L E V
248 52 39 125 247 syl3anc φ Z V Z 1 + L E V
249 eluzp1p1 Z V Z 1 + L E V Z V + 1 Z 1 + L E V + 1
250 248 249 syl φ Z V + 1 Z 1 + L E V + 1
251 hashfzo Z V + 1 Z 1 + L E V + 1 Z 1 + L E V + 1 ..^ Z V + 1 = Z V + 1 - Z 1 + L E V + 1
252 250 251 syl φ Z 1 + L E V + 1 ..^ Z V + 1 = Z V + 1 - Z 1 + L E V + 1
253 62 recnd φ Z V
254 253 55 56 pnpcan2d φ Z V + 1 - Z 1 + L E V + 1 = Z V Z 1 + L E V
255 246 252 254 3eqtrd φ I = Z V Z 1 + L E V
256 241 255 breqtrrd φ L E 4 Z V < I
257 40 45 256 ltled φ L E 4 Z V I
258 35 45 38 lemuldivd φ L E 4 Z V I L E 4 I Z V
259 257 258 mpbid φ L E 4 I Z V
260 21 rpred φ V
261 76 82 73 97 103 ltletrd φ 1 + L E V < Z
262 260 76 73 122 261 lttrd φ V < Z
263 260 73 262 ltled φ V Z
264 21 rprege0d φ V 0 V
265 72 rprege0d φ Z 0 Z
266 le2sq V 0 V Z 0 Z V Z V 2 Z 2
267 264 265 266 syl2anc φ V Z V 2 Z 2
268 263 267 mpbid φ V 2 Z 2
269 resqrtth Z 0 Z Z 2 = Z
270 107 269 syl φ Z 2 = Z
271 268 270 breqtrd φ V 2 Z
272 2z 2
273 rpexpcl V + 2 V 2 +
274 21 272 273 sylancl φ V 2 +
275 274 rpred φ V 2
276 275 111 37 lemul2d φ V 2 Z Z V 2 Z Z
277 271 276 mpbid φ Z V 2 Z Z
278 221 sqvald φ Z 2 = Z Z
279 277 278 breqtrrd φ Z V 2 Z 2
280 111 resqcld φ Z 2
281 111 280 274 lemuldivd φ Z V 2 Z 2 Z Z 2 V 2
282 279 281 mpbid φ Z Z 2 V 2
283 21 rpne0d φ V 0
284 221 114 283 sqdivd φ Z V 2 = Z 2 V 2
285 282 284 breqtrrd φ Z Z V 2
286 rpexpcl Z V + 2 Z V 2 +
287 38 272 286 sylancl φ Z V 2 +
288 37 287 logled φ Z Z V 2 log Z log Z V 2
289 285 288 mpbid φ log Z log Z V 2
290 relogexp Z V + 2 log Z V 2 = 2 log Z V
291 38 272 290 sylancl φ log Z V 2 = 2 log Z V
292 289 291 breqtrd φ log Z 2 log Z V
293 37 relogcld φ log Z
294 38 relogcld φ log Z V
295 ledivmul log Z log Z V 2 0 < 2 log Z 2 log Z V log Z 2 log Z V
296 293 294 193 195 295 syl112anc φ log Z 2 log Z V log Z 2 log Z V
297 292 296 mpbird φ log Z 2 log Z V
298 34 rprege0d φ L E 4 0 L E 4
299 45 38 rerpdivcld φ I Z V
300 36 simp2d φ 1 < Z e Z Z Z Y
301 300 simp1d φ 1 < Z
302 111 301 rplogcld φ log Z +
303 302 rphalfcld φ log Z 2 +
304 303 rprege0d φ log Z 2 0 log Z 2
305 lemul12a L E 4 0 L E 4 I Z V log Z 2 0 log Z 2 log Z V L E 4 I Z V log Z 2 log Z V L E 4 log Z 2 I Z V log Z V
306 298 299 304 294 305 syl22anc φ L E 4 I Z V log Z 2 log Z V L E 4 log Z 2 I Z V log Z V
307 259 297 306 mp2and φ L E 4 log Z 2 I Z V log Z V
308 302 rpcnd φ log Z
309 8nn 8
310 nnrp 8 8 +
311 309 310 ax-mp 8 +
312 rpcnne0 8 + 8 8 0
313 311 312 mp1i φ 8 8 0
314 div23 L E log Z 8 8 0 L E log Z 8 = L E 8 log Z
315 150 308 313 314 syl3anc φ L E log Z 8 = L E 8 log Z
316 divmuldiv L E log Z 4 4 0 2 2 0 L E 4 log Z 2 = L E log Z 4 2
317 150 308 143 153 316 syl22anc φ L E 4 log Z 2 = L E log Z 4 2
318 4t2e8 4 2 = 8
319 318 oveq2i L E log Z 4 2 = L E log Z 8
320 317 319 eqtr2di φ L E log Z 8 = L E 4 log Z 2
321 315 320 eqtr3d φ L E 8 log Z = L E 4 log Z 2
322 45 recnd φ I
323 294 recnd φ log Z V
324 38 rpcnne0d φ Z V Z V 0
325 divass I log Z V Z V Z V 0 I log Z V Z V = I log Z V Z V
326 div23 I log Z V Z V Z V 0 I log Z V Z V = I Z V log Z V
327 325 326 eqtr3d I log Z V Z V Z V 0 I log Z V Z V = I Z V log Z V
328 322 323 324 327 syl3anc φ I log Z V Z V = I Z V log Z V
329 307 321 328 3brtr4d φ L E 8 log Z I log Z V Z V
330 rpdivcl L E + 8 + L E 8 +
331 29 311 330 sylancl φ L E 8 +
332 331 302 rpmulcld φ L E 8 log Z +
333 332 rpred φ L E 8 log Z
334 294 38 rerpdivcld φ log Z V Z V
335 45 334 remulcld φ I log Z V Z V
336 183 simp3d φ U E +
337 333 335 336 lemul2d φ L E 8 log Z I log Z V Z V U E L E 8 log Z U E I log Z V Z V
338 329 337 mpbid φ U E L E 8 log Z U E I log Z V Z V
339 336 rpcnd φ U E
340 334 recnd φ log Z V Z V
341 339 322 340 mul12d φ U E I log Z V Z V = I U E log Z V Z V
342 338 341 breqtrd φ U E L E 8 log Z I U E log Z V Z V