Metamath Proof Explorer


Theorem pntlemf

Description: Lemma for pnt . Add up the pieces in pntlemi to get an estimate slightly better than the naive lower bound 0 . (Contributed by Mario Carneiro, 13-Apr-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
Assertion pntlemf φ U E L E 2 32 B log Z 2 n = 1 Z Y U n R Z n Z log n

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 1 2 3 4 5 6 7 8 9 10 pntlemc φ E + K + E 0 1 1 < K U E +
21 20 simp3d φ E 0 1 1 < K U E +
22 21 simp3d φ U E +
23 1 2 3 4 5 6 pntlemd φ L + D + F +
24 23 simp1d φ L +
25 20 simp1d φ E +
26 2z 2
27 rpexpcl E + 2 E 2 +
28 25 26 27 sylancl φ E 2 +
29 24 28 rpmulcld φ L E 2 +
30 3nn0 3 0
31 2nn 2
32 30 31 decnncl 32
33 nnrp 32 32 +
34 32 33 ax-mp 32 +
35 rpmulcl 32 + B + 32 B +
36 34 3 35 sylancr φ 32 B +
37 29 36 rpdivcld φ L E 2 32 B +
38 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
39 38 simp1d φ Z +
40 39 rpred φ Z
41 38 simp2d φ 1 < Z e Z Z Z Y
42 41 simp1d φ 1 < Z
43 40 42 rplogcld φ log Z +
44 rpexpcl log Z + 2 log Z 2 +
45 43 26 44 sylancl φ log Z 2 +
46 37 45 rpmulcld φ L E 2 32 B log Z 2 +
47 22 46 rpmulcld φ U E L E 2 32 B log Z 2 +
48 47 rpred φ U E L E 2 32 B log Z 2
49 24 25 rpmulcld φ L E +
50 8re 8
51 8pos 0 < 8
52 50 51 elrpii 8 +
53 rpdivcl L E + 8 + L E 8 +
54 49 52 53 sylancl φ L E 8 +
55 54 43 rpmulcld φ L E 8 log Z +
56 22 55 rpmulcld φ U E L E 8 log Z +
57 56 rpred φ U E L E 8 log Z
58 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
59 58 simp1d φ M
60 58 simp2d φ N M
61 eluznn M N M N
62 59 60 61 syl2anc φ N
63 62 nnred φ N
64 59 nnred φ M
65 63 64 resubcld φ N M
66 57 65 remulcld φ U E L E 8 log Z N M
67 fzfid φ 1 Z Y Fin
68 7 rpred φ U
69 elfznn n 1 Z Y n
70 nndivre U n U n
71 68 69 70 syl2an φ n 1 Z Y U n
72 39 adantr φ n 1 Z Y Z +
73 69 adantl φ n 1 Z Y n
74 73 nnrpd φ n 1 Z Y n +
75 72 74 rpdivcld φ n 1 Z Y Z n +
76 1 pntrf R : +
77 76 ffvelrni Z n + R Z n
78 75 77 syl φ n 1 Z Y R Z n
79 78 72 rerpdivcld φ n 1 Z Y R Z n Z
80 79 recnd φ n 1 Z Y R Z n Z
81 80 abscld φ n 1 Z Y R Z n Z
82 71 81 resubcld φ n 1 Z Y U n R Z n Z
83 74 relogcld φ n 1 Z Y log n
84 82 83 remulcld φ n 1 Z Y U n R Z n Z log n
85 67 84 fsumrecl φ n = 1 Z Y U n R Z n Z log n
86 49 rpcnd φ L E
87 20 simp2d φ K +
88 87 rpred φ K
89 21 simp2d φ 1 < K
90 88 89 rplogcld φ log K +
91 43 90 rpdivcld φ log Z log K +
92 91 rpcnd φ log Z log K
93 rpcnne0 8 + 8 8 0
94 52 93 mp1i φ 8 8 0
95 4re 4
96 4pos 0 < 4
97 95 96 elrpii 4 +
98 rpcnne0 4 + 4 4 0
99 97 98 mp1i φ 4 4 0
100 divmuldiv L E log Z log K 8 8 0 4 4 0 L E 8 log Z log K 4 = L E log Z log K 8 4
101 86 92 94 99 100 syl22anc φ L E 8 log Z log K 4 = L E log Z log K 8 4
102 10 fveq2i log K = log e B E
103 3 25 rpdivcld φ B E +
104 103 rpred φ B E
105 104 relogefd φ log e B E = B E
106 102 105 syl5eq φ log K = B E
107 106 oveq2d φ log Z log K = log Z B E
108 43 rpcnd φ log Z
109 3 rpcnne0d φ B B 0
110 25 rpcnne0d φ E E 0
111 divdiv2 log Z B B 0 E E 0 log Z B E = log Z E B
112 108 109 110 111 syl3anc φ log Z B E = log Z E B
113 107 112 eqtrd φ log Z log K = log Z E B
114 113 oveq2d φ L E log Z log K = L E log Z E B
115 25 rpcnd φ E
116 108 115 mulcld φ log Z E
117 divass L E log Z E B B 0 L E log Z E B = L E log Z E B
118 86 116 109 117 syl3anc φ L E log Z E B = L E log Z E B
119 24 rpcnd φ L
120 119 115 108 115 mul4d φ L E log Z E = L log Z E E
121 115 sqvald φ E 2 = E E
122 121 oveq2d φ L log Z E 2 = L log Z E E
123 115 sqcld φ E 2
124 119 108 123 mul32d φ L log Z E 2 = L E 2 log Z
125 120 122 124 3eqtr2d φ L E log Z E = L E 2 log Z
126 125 oveq1d φ L E log Z E B = L E 2 log Z B
127 114 118 126 3eqtr2d φ L E log Z log K = L E 2 log Z B
128 8t4e32 8 4 = 32
129 128 a1i φ 8 4 = 32
130 127 129 oveq12d φ L E log Z log K 8 4 = L E 2 log Z B 32
131 29 rpcnd φ L E 2
132 131 108 mulcld φ L E 2 log Z
133 rpcnne0 32 + 32 32 0
134 34 133 mp1i φ 32 32 0
135 divdiv1 L E 2 log Z B B 0 32 32 0 L E 2 log Z B 32 = L E 2 log Z B 32
136 132 109 134 135 syl3anc φ L E 2 log Z B 32 = L E 2 log Z B 32
137 32 nncni 32
138 3 rpcnd φ B
139 mulcom 32 B 32 B = B 32
140 137 138 139 sylancr φ 32 B = B 32
141 140 oveq2d φ L E 2 log Z 32 B = L E 2 log Z B 32
142 36 rpcnne0d φ 32 B 32 B 0
143 div23 L E 2 log Z 32 B 32 B 0 L E 2 log Z 32 B = L E 2 32 B log Z
144 131 108 142 143 syl3anc φ L E 2 log Z 32 B = L E 2 32 B log Z
145 136 141 144 3eqtr2d φ L E 2 log Z B 32 = L E 2 32 B log Z
146 101 130 145 3eqtrd φ L E 8 log Z log K 4 = L E 2 32 B log Z
147 146 oveq1d φ L E 8 log Z log K 4 log Z = L E 2 32 B log Z log Z
148 54 rpcnd φ L E 8
149 91 rpred φ log Z log K
150 4nn 4
151 nndivre log Z log K 4 log Z log K 4
152 149 150 151 sylancl φ log Z log K 4
153 152 recnd φ log Z log K 4
154 148 108 153 mul32d φ L E 8 log Z log Z log K 4 = L E 8 log Z log K 4 log Z
155 108 sqvald φ log Z 2 = log Z log Z
156 155 oveq2d φ L E 2 32 B log Z 2 = L E 2 32 B log Z log Z
157 37 rpcnd φ L E 2 32 B
158 157 108 108 mulassd φ L E 2 32 B log Z log Z = L E 2 32 B log Z log Z
159 156 158 eqtr4d φ L E 2 32 B log Z 2 = L E 2 32 B log Z log Z
160 147 154 159 3eqtr4d φ L E 8 log Z log Z log K 4 = L E 2 32 B log Z 2
161 58 simp3d φ log Z log K 4 N M
162 152 65 55 lemul2d φ log Z log K 4 N M L E 8 log Z log Z log K 4 L E 8 log Z N M
163 161 162 mpbid φ L E 8 log Z log Z log K 4 L E 8 log Z N M
164 160 163 eqbrtrrd φ L E 2 32 B log Z 2 L E 8 log Z N M
165 46 rpred φ L E 2 32 B log Z 2
166 55 rpred φ L E 8 log Z
167 166 65 remulcld φ L E 8 log Z N M
168 165 167 22 lemul2d φ L E 2 32 B log Z 2 L E 8 log Z N M U E L E 2 32 B log Z 2 U E L E 8 log Z N M
169 164 168 mpbid φ U E L E 2 32 B log Z 2 U E L E 8 log Z N M
170 22 rpcnd φ U E
171 55 rpcnd φ L E 8 log Z
172 65 recnd φ N M
173 170 171 172 mulassd φ U E L E 8 log Z N M = U E L E 8 log Z N M
174 169 173 breqtrrd φ U E L E 2 32 B log Z 2 U E L E 8 log Z N M
175 fzfid φ Z K N + 1 Z Y Fin
176 62 nnzd φ N
177 87 176 rpexpcld φ K N +
178 39 177 rpdivcld φ Z K N +
179 178 rprege0d φ Z K N 0 Z K N
180 flge0nn0 Z K N 0 Z K N Z K N 0
181 nn0p1nn Z K N 0 Z K N + 1
182 179 180 181 3syl φ Z K N + 1
183 nnuz = 1
184 182 183 eleqtrdi φ Z K N + 1 1
185 fzss1 Z K N + 1 1 Z K N + 1 Z Y 1 Z Y
186 184 185 syl φ Z K N + 1 Z Y 1 Z Y
187 186 sselda φ n Z K N + 1 Z Y n 1 Z Y
188 187 84 syldan φ n Z K N + 1 Z Y U n R Z n Z log n
189 175 188 fsumrecl φ n = Z K N + 1 Z Y U n R Z n Z log n
190 eluzfz2 N M N M N
191 60 190 syl φ N M N
192 oveq1 m = M m M = M M
193 192 oveq2d m = M U E L E 8 log Z m M = U E L E 8 log Z M M
194 oveq2 m = M K m = K M
195 194 oveq2d m = M Z K m = Z K M
196 195 fveq2d m = M Z K m = Z K M
197 196 oveq1d m = M Z K m + 1 = Z K M + 1
198 197 oveq1d m = M Z K m + 1 Z Y = Z K M + 1 Z Y
199 198 sumeq1d m = M n = Z K m + 1 Z Y U n R Z n Z log n = n = Z K M + 1 Z Y U n R Z n Z log n
200 193 199 breq12d m = M U E L E 8 log Z m M n = Z K m + 1 Z Y U n R Z n Z log n U E L E 8 log Z M M n = Z K M + 1 Z Y U n R Z n Z log n
201 200 imbi2d m = M φ U E L E 8 log Z m M n = Z K m + 1 Z Y U n R Z n Z log n φ U E L E 8 log Z M M n = Z K M + 1 Z Y U n R Z n Z log n
202 oveq1 m = j m M = j M
203 202 oveq2d m = j U E L E 8 log Z m M = U E L E 8 log Z j M
204 oveq2 m = j K m = K j
205 204 oveq2d m = j Z K m = Z K j
206 205 fveq2d m = j Z K m = Z K j
207 206 oveq1d m = j Z K m + 1 = Z K j + 1
208 207 oveq1d m = j Z K m + 1 Z Y = Z K j + 1 Z Y
209 208 sumeq1d m = j n = Z K m + 1 Z Y U n R Z n Z log n = n = Z K j + 1 Z Y U n R Z n Z log n
210 203 209 breq12d m = j U E L E 8 log Z m M n = Z K m + 1 Z Y U n R Z n Z log n U E L E 8 log Z j M n = Z K j + 1 Z Y U n R Z n Z log n
211 210 imbi2d m = j φ U E L E 8 log Z m M n = Z K m + 1 Z Y U n R Z n Z log n φ U E L E 8 log Z j M n = Z K j + 1 Z Y U n R Z n Z log n
212 oveq1 m = j + 1 m M = j + 1 - M
213 212 oveq2d m = j + 1 U E L E 8 log Z m M = U E L E 8 log Z j + 1 - M
214 oveq2 m = j + 1 K m = K j + 1
215 214 oveq2d m = j + 1 Z K m = Z K j + 1
216 215 fveq2d m = j + 1 Z K m = Z K j + 1
217 216 oveq1d m = j + 1 Z K m + 1 = Z K j + 1 + 1
218 217 oveq1d m = j + 1 Z K m + 1 Z Y = Z K j + 1 + 1 Z Y
219 218 sumeq1d m = j + 1 n = Z K m + 1 Z Y U n R Z n Z log n = n = Z K j + 1 + 1 Z Y U n R Z n Z log n
220 213 219 breq12d m = j + 1 U E L E 8 log Z m M n = Z K m + 1 Z Y U n R Z n Z log n U E L E 8 log Z j + 1 - M n = Z K j + 1 + 1 Z Y U n R Z n Z log n
221 220 imbi2d m = j + 1 φ U E L E 8 log Z m M n = Z K m + 1 Z Y U n R Z n Z log n φ U E L E 8 log Z j + 1 - M n = Z K j + 1 + 1 Z Y U n R Z n Z log n
222 oveq1 m = N m M = N M
223 222 oveq2d m = N U E L E 8 log Z m M = U E L E 8 log Z N M
224 oveq2 m = N K m = K N
225 224 oveq2d m = N Z K m = Z K N
226 225 fveq2d m = N Z K m = Z K N
227 226 oveq1d m = N Z K m + 1 = Z K N + 1
228 227 oveq1d m = N Z K m + 1 Z Y = Z K N + 1 Z Y
229 228 sumeq1d m = N n = Z K m + 1 Z Y U n R Z n Z log n = n = Z K N + 1 Z Y U n R Z n Z log n
230 223 229 breq12d m = N U E L E 8 log Z m M n = Z K m + 1 Z Y U n R Z n Z log n U E L E 8 log Z N M n = Z K N + 1 Z Y U n R Z n Z log n
231 230 imbi2d m = N φ U E L E 8 log Z m M n = Z K m + 1 Z Y U n R Z n Z log n φ U E L E 8 log Z N M n = Z K N + 1 Z Y U n R Z n Z log n
232 59 nncnd φ M
233 232 subidd φ M M = 0
234 233 oveq2d φ U E L E 8 log Z M M = U E L E 8 log Z 0
235 56 rpcnd φ U E L E 8 log Z
236 235 mul01d φ U E L E 8 log Z 0 = 0
237 234 236 eqtrd φ U E L E 8 log Z M M = 0
238 fzfid φ Z K M + 1 Z Y Fin
239 59 nnzd φ M
240 87 239 rpexpcld φ K M +
241 39 240 rpdivcld φ Z K M +
242 241 rprege0d φ Z K M 0 Z K M
243 flge0nn0 Z K M 0 Z K M Z K M 0
244 nn0p1nn Z K M 0 Z K M + 1
245 242 243 244 3syl φ Z K M + 1
246 245 183 eleqtrdi φ Z K M + 1 1
247 fzss1 Z K M + 1 1 Z K M + 1 Z Y 1 Z Y
248 246 247 syl φ Z K M + 1 Z Y 1 Z Y
249 248 sselda φ n Z K M + 1 Z Y n 1 Z Y
250 249 84 syldan φ n Z K M + 1 Z Y U n R Z n Z log n
251 elfzle2 n 1 Z Y n Z Y
252 251 adantl φ n 1 Z Y n Z Y
253 11 simpld φ Y +
254 39 253 rpdivcld φ Z Y +
255 254 rpred φ Z Y
256 elfzelz n 1 Z Y n
257 flge Z Y n n Z Y n Z Y
258 255 256 257 syl2an φ n 1 Z Y n Z Y n Z Y
259 252 258 mpbird φ n 1 Z Y n Z Y
260 73 259 jca φ n 1 Z Y n n Z Y
261 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 pntlemn φ n n Z Y 0 U n R Z n Z log n
262 260 261 syldan φ n 1 Z Y 0 U n R Z n Z log n
263 249 262 syldan φ n Z K M + 1 Z Y 0 U n R Z n Z log n
264 238 250 263 fsumge0 φ 0 n = Z K M + 1 Z Y U n R Z n Z log n
265 237 264 eqbrtrd φ U E L E 8 log Z M M n = Z K M + 1 Z Y U n R Z n Z log n
266 265 a1i N M φ U E L E 8 log Z M M n = Z K M + 1 Z Y U n R Z n Z log n
267 eqid Z K j + 1 + 1 Z K j = Z K j + 1 + 1 Z K j
268 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 267 pntlemi φ j M ..^ N U E L E 8 log Z n = Z K j + 1 + 1 Z K j U n R Z n Z log n
269 56 adantr φ j M ..^ N U E L E 8 log Z +
270 269 rpred φ j M ..^ N U E L E 8 log Z
271 elfzoelz j M ..^ N j
272 271 adantl φ j M ..^ N j
273 272 zred φ j M ..^ N j
274 59 adantr φ j M ..^ N M
275 274 nnred φ j M ..^ N M
276 273 275 resubcld φ j M ..^ N j M
277 270 276 remulcld φ j M ..^ N U E L E 8 log Z j M
278 fzfid φ j M ..^ N Z K j + 1 + 1 Z K j Fin
279 ssun1 Z K j + 1 + 1 Z K j Z K j + 1 + 1 Z K j Z K j + 1 Z Y
280 40 adantr φ j M ..^ N Z
281 87 adantr φ j M ..^ N K +
282 272 peano2zd φ j M ..^ N j + 1
283 281 282 rpexpcld φ j M ..^ N K j + 1 +
284 280 283 rerpdivcld φ j M ..^ N Z K j + 1
285 281 272 rpexpcld φ j M ..^ N K j +
286 280 285 rerpdivcld φ j M ..^ N Z K j
287 88 adantr φ j M ..^ N K
288 1re 1
289 ltle 1 K 1 < K 1 K
290 288 88 289 sylancr φ 1 < K 1 K
291 89 290 mpd φ 1 K
292 291 adantr φ j M ..^ N 1 K
293 uzid j j j
294 peano2uz j j j + 1 j
295 272 293 294 3syl φ j M ..^ N j + 1 j
296 287 292 295 leexp2ad φ j M ..^ N K j K j + 1
297 39 adantr φ j M ..^ N Z +
298 285 283 297 lediv2d φ j M ..^ N K j K j + 1 Z K j + 1 Z K j
299 296 298 mpbid φ j M ..^ N Z K j + 1 Z K j
300 flword2 Z K j + 1 Z K j Z K j + 1 Z K j Z K j Z K j + 1
301 284 286 299 300 syl3anc φ j M ..^ N Z K j Z K j + 1
302 eluzp1p1 Z K j Z K j + 1 Z K j + 1 Z K j + 1 + 1
303 301 302 syl φ j M ..^ N Z K j + 1 Z K j + 1 + 1
304 286 flcld φ j M ..^ N Z K j
305 254 adantr φ j M ..^ N Z Y +
306 305 rpred φ j M ..^ N Z Y
307 306 flcld φ j M ..^ N Z Y
308 253 adantr φ j M ..^ N Y +
309 308 rpred φ j M ..^ N Y
310 285 rpred φ j M ..^ N K j
311 12 simpld φ X +
312 311 rpred φ X
313 312 adantr φ j M ..^ N X
314 12 simprd φ Y < X
315 314 adantr φ j M ..^ N Y < X
316 elfzofz j M ..^ N j M N
317 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemh φ j M N X < K j K j Z
318 316 317 sylan2 φ j M ..^ N X < K j K j Z
319 318 simpld φ j M ..^ N X < K j
320 309 313 310 315 319 lttrd φ j M ..^ N Y < K j
321 309 310 320 ltled φ j M ..^ N Y K j
322 308 285 297 lediv2d φ j M ..^ N Y K j Z K j Z Y
323 321 322 mpbid φ j M ..^ N Z K j Z Y
324 flwordi Z K j Z Y Z K j Z Y Z K j Z Y
325 286 306 323 324 syl3anc φ j M ..^ N Z K j Z Y
326 eluz2 Z Y Z K j Z K j Z Y Z K j Z Y
327 304 307 325 326 syl3anbrc φ j M ..^ N Z Y Z K j
328 fzsplit2 Z K j + 1 Z K j + 1 + 1 Z Y Z K j Z K j + 1 + 1 Z Y = Z K j + 1 + 1 Z K j Z K j + 1 Z Y
329 303 327 328 syl2anc φ j M ..^ N Z K j + 1 + 1 Z Y = Z K j + 1 + 1 Z K j Z K j + 1 Z Y
330 279 329 sseqtrrid φ j M ..^ N Z K j + 1 + 1 Z K j Z K j + 1 + 1 Z Y
331 297 283 rpdivcld φ j M ..^ N Z K j + 1 +
332 331 rprege0d φ j M ..^ N Z K j + 1 0 Z K j + 1
333 flge0nn0 Z K j + 1 0 Z K j + 1 Z K j + 1 0
334 nn0p1nn Z K j + 1 0 Z K j + 1 + 1
335 332 333 334 3syl φ j M ..^ N Z K j + 1 + 1
336 335 183 eleqtrdi φ j M ..^ N Z K j + 1 + 1 1
337 fzss1 Z K j + 1 + 1 1 Z K j + 1 + 1 Z Y 1 Z Y
338 336 337 syl φ j M ..^ N Z K j + 1 + 1 Z Y 1 Z Y
339 330 338 sstrd φ j M ..^ N Z K j + 1 + 1 Z K j 1 Z Y
340 339 sselda φ j M ..^ N n Z K j + 1 + 1 Z K j n 1 Z Y
341 84 adantlr φ j M ..^ N n 1 Z Y U n R Z n Z log n
342 340 341 syldan φ j M ..^ N n Z K j + 1 + 1 Z K j U n R Z n Z log n
343 278 342 fsumrecl φ j M ..^ N n = Z K j + 1 + 1 Z K j U n R Z n Z log n
344 fzfid φ j M ..^ N Z K j + 1 Z Y Fin
345 ssun2 Z K j + 1 Z Y Z K j + 1 + 1 Z K j Z K j + 1 Z Y
346 345 329 sseqtrrid φ j M ..^ N Z K j + 1 Z Y Z K j + 1 + 1 Z Y
347 346 338 sstrd φ j M ..^ N Z K j + 1 Z Y 1 Z Y
348 347 sselda φ j M ..^ N n Z K j + 1 Z Y n 1 Z Y
349 348 341 syldan φ j M ..^ N n Z K j + 1 Z Y U n R Z n Z log n
350 344 349 fsumrecl φ j M ..^ N n = Z K j + 1 Z Y U n R Z n Z log n
351 le2add U E L E 8 log Z U E L E 8 log Z j M n = Z K j + 1 + 1 Z K j U n R Z n Z log n n = Z K j + 1 Z Y U n R Z n Z log n U E L E 8 log Z n = Z K j + 1 + 1 Z K j U n R Z n Z log n U E L E 8 log Z j M n = Z K j + 1 Z Y U n R Z n Z log n U E L E 8 log Z + U E L E 8 log Z j M n = Z K j + 1 + 1 Z K j U n R Z n Z log n + n = Z K j + 1 Z Y U n R Z n Z log n
352 270 277 343 350 351 syl22anc φ j M ..^ N U E L E 8 log Z n = Z K j + 1 + 1 Z K j U n R Z n Z log n U E L E 8 log Z j M n = Z K j + 1 Z Y U n R Z n Z log n U E L E 8 log Z + U E L E 8 log Z j M n = Z K j + 1 + 1 Z K j U n R Z n Z log n + n = Z K j + 1 Z Y U n R Z n Z log n
353 268 352 mpand φ j M ..^ N U E L E 8 log Z j M n = Z K j + 1 Z Y U n R Z n Z log n U E L E 8 log Z + U E L E 8 log Z j M n = Z K j + 1 + 1 Z K j U n R Z n Z log n + n = Z K j + 1 Z Y U n R Z n Z log n
354 235 adantr φ j M ..^ N U E L E 8 log Z
355 1cnd φ j M ..^ N 1
356 272 zcnd φ j M ..^ N j
357 232 adantr φ j M ..^ N M
358 356 357 subcld φ j M ..^ N j M
359 354 355 358 adddid φ j M ..^ N U E L E 8 log Z 1 + j - M = U E L E 8 log Z 1 + U E L E 8 log Z j M
360 355 358 addcomd φ j M ..^ N 1 + j - M = j - M + 1
361 356 355 357 addsubd φ j M ..^ N j + 1 - M = j - M + 1
362 360 361 eqtr4d φ j M ..^ N 1 + j - M = j + 1 - M
363 362 oveq2d φ j M ..^ N U E L E 8 log Z 1 + j - M = U E L E 8 log Z j + 1 - M
364 354 mulid1d φ j M ..^ N U E L E 8 log Z 1 = U E L E 8 log Z
365 364 oveq1d φ j M ..^ N U E L E 8 log Z 1 + U E L E 8 log Z j M = U E L E 8 log Z + U E L E 8 log Z j M
366 359 363 365 3eqtr3d φ j M ..^ N U E L E 8 log Z j + 1 - M = U E L E 8 log Z + U E L E 8 log Z j M
367 reflcl Z K j Z K j
368 286 367 syl φ j M ..^ N Z K j
369 368 ltp1d φ j M ..^ N Z K j < Z K j + 1
370 fzdisj Z K j < Z K j + 1 Z K j + 1 + 1 Z K j Z K j + 1 Z Y =
371 369 370 syl φ j M ..^ N Z K j + 1 + 1 Z K j Z K j + 1 Z Y =
372 fzfid φ j M ..^ N Z K j + 1 + 1 Z Y Fin
373 338 sselda φ j M ..^ N n Z K j + 1 + 1 Z Y n 1 Z Y
374 373 341 syldan φ j M ..^ N n Z K j + 1 + 1 Z Y U n R Z n Z log n
375 374 recnd φ j M ..^ N n Z K j + 1 + 1 Z Y U n R Z n Z log n
376 371 329 372 375 fsumsplit φ j M ..^ N n = Z K j + 1 + 1 Z Y U n R Z n Z log n = n = Z K j + 1 + 1 Z K j U n R Z n Z log n + n = Z K j + 1 Z Y U n R Z n Z log n
377 366 376 breq12d φ j M ..^ N U E L E 8 log Z j + 1 - M n = Z K j + 1 + 1 Z Y U n R Z n Z log n U E L E 8 log Z + U E L E 8 log Z j M n = Z K j + 1 + 1 Z K j U n R Z n Z log n + n = Z K j + 1 Z Y U n R Z n Z log n
378 353 377 sylibrd φ j M ..^ N U E L E 8 log Z j M n = Z K j + 1 Z Y U n R Z n Z log n U E L E 8 log Z j + 1 - M n = Z K j + 1 + 1 Z Y U n R Z n Z log n
379 378 expcom j M ..^ N φ U E L E 8 log Z j M n = Z K j + 1 Z Y U n R Z n Z log n U E L E 8 log Z j + 1 - M n = Z K j + 1 + 1 Z Y U n R Z n Z log n
380 379 a2d j M ..^ N φ U E L E 8 log Z j M n = Z K j + 1 Z Y U n R Z n Z log n φ U E L E 8 log Z j + 1 - M n = Z K j + 1 + 1 Z Y U n R Z n Z log n
381 201 211 221 231 266 380 fzind2 N M N φ U E L E 8 log Z N M n = Z K N + 1 Z Y U n R Z n Z log n
382 191 381 mpcom φ U E L E 8 log Z N M n = Z K N + 1 Z Y U n R Z n Z log n
383 67 84 262 186 fsumless φ n = Z K N + 1 Z Y U n R Z n Z log n n = 1 Z Y U n R Z n Z log n
384 66 189 85 382 383 letrd φ U E L E 8 log Z N M n = 1 Z Y U n R Z n Z log n
385 48 66 85 174 384 letrd φ U E L E 2 32 B log Z 2 n = 1 Z Y U n R Z n Z log n