Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pntlemf Structured version   Visualization version   Unicode version

Theorem pntlemf 24522
 Description: Lemma for pnt 24531. Add up the pieces in pntlemi 24521 to get an estimate slightly better than the naive lower bound . (Contributed by Mario Carneiro, 13-Apr-2016.)
Hypotheses
Ref Expression
pntlem1.r ψ
pntlem1.a
pntlem1.b
pntlem1.l
pntlem1.d
pntlem1.f ;
pntlem1.u
pntlem1.u2
pntlem1.e
pntlem1.k
pntlem1.y
pntlem1.x
pntlem1.c
pntlem1.w ;
pntlem1.z
pntlem1.m
pntlem1.n
pntlem1.U
pntlem1.K
Assertion
Ref Expression
pntlemf ;
Distinct variable groups:   ,   ,,,,   ,,,   ,,   ,   ,,   ,,,,   ,,   ,,   ,,,   ,,   ,,,,,   ,,,
Allowed substitution hints:   (,,,)   (,,,,)   (,,,,)   (,,,)   (,,,,)   ()   (,,)   (,,,,)   (,)   ()   (,,)   (,,)   (,,)   (,)   (,,)   (,)

Proof of Theorem pntlemf
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pntlem1.r . . . . . . 7 ψ
2 pntlem1.a . . . . . . 7
3 pntlem1.b . . . . . . 7
4 pntlem1.l . . . . . . 7
5 pntlem1.d . . . . . . 7
6 pntlem1.f . . . . . . 7 ;
7 pntlem1.u . . . . . . 7
8 pntlem1.u2 . . . . . . 7
9 pntlem1.e . . . . . . 7
10 pntlem1.k . . . . . . 7
111, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 24512 . . . . . 6
1211simp3d 1044 . . . . 5
1312simp3d 1044 . . . 4
141, 2, 3, 4, 5, 6pntlemd 24511 . . . . . . . 8
1514simp1d 1042 . . . . . . 7
1611simp1d 1042 . . . . . . . 8
17 2z 10993 . . . . . . . 8
18 rpexpcl 12329 . . . . . . . 8
1916, 17, 18sylancl 675 . . . . . . 7
2015, 19rpmulcld 11380 . . . . . 6
21 3nn0 10911 . . . . . . . . 9
22 2nn 10790 . . . . . . . . 9
2321, 22decnncl 11087 . . . . . . . 8 ;
24 nnrp 11334 . . . . . . . 8 ; ;
2523, 24ax-mp 5 . . . . . . 7 ;
26 rpmulcl 11347 . . . . . . 7 ; ;
2725, 3, 26sylancr 676 . . . . . 6 ;
2820, 27rpdivcld 11381 . . . . 5 ;
29 pntlem1.y . . . . . . . . . 10
30 pntlem1.x . . . . . . . . . 10
31 pntlem1.c . . . . . . . . . 10
32 pntlem1.w . . . . . . . . . 10 ;
33 pntlem1.z . . . . . . . . . 10
341, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33pntlemb 24514 . . . . . . . . 9 ;
3534simp1d 1042 . . . . . . . 8
3635rpred 11364 . . . . . . 7
3734simp2d 1043 . . . . . . . 8
3837simp1d 1042 . . . . . . 7
3936, 38rplogcld 23657 . . . . . 6
40 rpexpcl 12329 . . . . . 6
4139, 17, 40sylancl 675 . . . . 5
4228, 41rpmulcld 11380 . . . 4 ;
4313, 42rpmulcld 11380 . . 3 ;
4443rpred 11364 . 2 ;
4515, 16rpmulcld 11380 . . . . . . 7
46 8re 10716 . . . . . . . 8
47 8pos 10732 . . . . . . . 8
4846, 47elrpii 11328 . . . . . . 7
49 rpdivcl 11348 . . . . . . 7
5045, 48, 49sylancl 675 . . . . . 6
5150, 39rpmulcld 11380 . . . . 5
5213, 51rpmulcld 11380 . . . 4
5352rpred 11364 . . 3
54 pntlem1.m . . . . . . . 8
55 pntlem1.n . . . . . . . 8
561, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55pntlemg 24515 . . . . . . 7
5756simp1d 1042 . . . . . 6
5856simp2d 1043 . . . . . 6
59 eluznn 11252 . . . . . 6
6057, 58, 59syl2anc 673 . . . . 5
6160nnred 10646 . . . 4
6257nnred 10646 . . . 4
6361, 62resubcld 10068 . . 3
6453, 63remulcld 9689 . 2
65 fzfid 12224 . . 3
667rpred 11364 . . . . . 6
67 elfznn 11854 . . . . . 6
68 nndivre 10667 . . . . . 6
6966, 67, 68syl2an 485 . . . . 5
7035adantr 472 . . . . . . . . . 10
7167adantl 473 . . . . . . . . . . 11
7271nnrpd 11362 . . . . . . . . . 10
7370, 72rpdivcld 11381 . . . . . . . . 9
741pntrf 24480 . . . . . . . . . 10
7574ffvelrni 6036 . . . . . . . . 9
7673, 75syl 17 . . . . . . . 8
7776, 70rerpdivcld 11392 . . . . . . 7
7877recnd 9687 . . . . . 6
7978abscld 13575 . . . . 5
8069, 79resubcld 10068 . . . 4
8172relogcld 23651 . . . 4
8280, 81remulcld 9689 . . 3
8365, 82fsumrecl 13877 . 2
8445rpcnd 11366 . . . . . . . . 9
8511simp2d 1043 . . . . . . . . . . . . 13
8685rpred 11364 . . . . . . . . . . . 12
8712simp2d 1043 . . . . . . . . . . . 12
8886, 87rplogcld 23657 . . . . . . . . . . 11
8939, 88rpdivcld 11381 . . . . . . . . . 10
9089rpcnd 11366 . . . . . . . . 9
91 rpcnne0 11342 . . . . . . . . . 10
9248, 91mp1i 13 . . . . . . . . 9
93 4re 10708 . . . . . . . . . . 11
94 4pos 10727 . . . . . . . . . . 11
9593, 94elrpii 11328 . . . . . . . . . 10
96 rpcnne0 11342 . . . . . . . . . 10
9795, 96mp1i 13 . . . . . . . . 9
98 divmuldiv 10329 . . . . . . . . 9
9984, 90, 92, 97, 98syl22anc 1293 . . . . . . . 8
10010fveq2i 5882 . . . . . . . . . . . . . 14
1013, 16rpdivcld 11381 . . . . . . . . . . . . . . . 16
102101rpred 11364 . . . . . . . . . . . . . . 15
103102relogefd 23656 . . . . . . . . . . . . . 14
104100, 103syl5eq 2517 . . . . . . . . . . . . 13
105104oveq2d 6324 . . . . . . . . . . . 12
10639rpcnd 11366 . . . . . . . . . . . . 13
1073rpcnne0d 11373 . . . . . . . . . . . . 13
10816rpcnne0d 11373 . . . . . . . . . . . . 13
109 divdiv2 10341 . . . . . . . . . . . . 13
110106, 107, 108, 109syl3anc 1292 . . . . . . . . . . . 12
111105, 110eqtrd 2505 . . . . . . . . . . 11
112111oveq2d 6324 . . . . . . . . . 10
11316rpcnd 11366 . . . . . . . . . . . 12
114106, 113mulcld 9681 . . . . . . . . . . 11
115 divass 10310 . . . . . . . . . . 11
11684, 114, 107, 115syl3anc 1292 . . . . . . . . . 10
11715rpcnd 11366 . . . . . . . . . . . . 13
118117, 113, 106, 113mul4d 9863 . . . . . . . . . . . 12
119113sqvald 12451 . . . . . . . . . . . . 13
120119oveq2d 6324 . . . . . . . . . . . 12
121113sqcld 12452 . . . . . . . . . . . . 13
122117, 106, 121mul32d 9861 . . . . . . . . . . . 12
123118, 120, 1223eqtr2d 2511 . . . . . . . . . . 11
124123oveq1d 6323 . . . . . . . . . 10
125112, 116, 1243eqtr2d 2511 . . . . . . . . 9
126 8t4e32 11164 . . . . . . . . . 10 ;
127126a1i 11 . . . . . . . . 9 ;
128125, 127oveq12d 6326 . . . . . . . 8 ;
12920rpcnd 11366 . . . . . . . . . . 11
130129, 106mulcld 9681 . . . . . . . . . 10
131 rpcnne0 11342 . . . . . . . . . . 11 ; ; ;
13225, 131mp1i 13 . . . . . . . . . 10 ; ;
133 divdiv1 10340 . . . . . . . . . 10 ; ; ; ;
134130, 107, 132, 133syl3anc 1292 . . . . . . . . 9 ; ;
13523nncni 10641 . . . . . . . . . . 11 ;
1363rpcnd 11366 . . . . . . . . . . 11
137 mulcom 9643 . . . . . . . . . . 11 ; ; ;
138135, 136, 137sylancr 676 . . . . . . . . . 10 ; ;
139138oveq2d 6324 . . . . . . . . 9 ; ;
14027rpcnne0d 11373 . . . . . . . . . 10 ; ;
141 div23 10311 . . . . . . . . . 10 ; ; ; ;
142129, 106, 140, 141syl3anc 1292 . . . . . . . . 9 ; ;
143134, 139, 1423eqtr2d 2511 . . . . . . . 8 ; ;
14499, 128, 1433eqtrd 2509 . . . . . . 7 ;
145144oveq1d 6323 . . . . . 6 ;
14650rpcnd 11366 . . . . . . 7
14789rpred 11364 . . . . . . . . 9
148 4nn 10792 . . . . . . . . 9
149 nndivre 10667 . . . . . . . . 9
150147, 148, 149sylancl 675 . . . . . . . 8
151150recnd 9687 . . . . . . 7
152146, 106, 151mul32d 9861 . . . . . 6
153106sqvald 12451 . . . . . . . 8
154153oveq2d 6324 . . . . . . 7 ; ;
15528rpcnd 11366 . . . . . . . 8 ;
156155, 106, 106mulassd 9684 . . . . . . 7 ; ;
157154, 156eqtr4d 2508 . . . . . 6 ; ;
158145, 152, 1573eqtr4d 2515 . . . . 5 ;
15956simp3d 1044 . . . . . 6
160150, 63, 51lemul2d 11405 . . . . . 6
161159, 160mpbid 215 . . . . 5
162158, 161eqbrtrrd 4418 . . . 4 ;
16342rpred 11364 . . . . 5 ;
16451rpred 11364 . . . . . 6
165164, 63remulcld 9689 . . . . 5
166163, 165, 13lemul2d 11405 . . . 4 ; ;
167162, 166mpbid 215 . . 3 ;
16813rpcnd 11366 . . . 4
16951rpcnd 11366 . . . 4
17063recnd 9687 . . . 4
171168, 169, 170mulassd 9684 . . 3
172167, 171breqtrrd 4422 . 2 ;
173 fzfid 12224 . . . 4
17460nnzd 11062 . . . . . . . . . . . 12
17585, 174rpexpcld 12477 . . . . . . . . . . 11
17635, 175rpdivcld 11381 . . . . . . . . . 10
177176rprege0d 11371 . . . . . . . . 9
178 flge0nn0 12087 . . . . . . . . 9
179 nn0p1nn 10933 . . . . . . . . 9
180177, 178, 1793syl 18 . . . . . . . 8
181 nnuz 11218 . . . . . . . 8
182180, 181syl6eleq 2559 . . . . . . 7
183 fzss1 11863 . . . . . . 7
184182, 183syl 17 . . . . . 6
185184sselda 3418 . . . . 5
186185, 82syldan 478 . . . 4
187173, 186fsumrecl 13877 . . 3
188 eluzfz2 11833 . . . . 5
18958, 188syl 17 . . . 4
190 oveq1 6315 . . . . . . . 8
191190oveq2d 6324 . . . . . . 7
192 oveq2 6316 . . . . . . . . . . . 12
193192oveq2d 6324 . . . . . . . . . . 11
194193fveq2d 5883 . . . . . . . . . 10
195194oveq1d 6323 . . . . . . . . 9
196195oveq1d 6323 . . . . . . . 8
197196sumeq1d 13844 . . . . . . 7
198191, 197breq12d 4408 . . . . . 6
199198imbi2d 323 . . . . 5
200 oveq1 6315 . . . . . . . 8
201200oveq2d 6324 . . . . . . 7
202 oveq2 6316 . . . . . . . . . . . 12
203202oveq2d 6324 . . . . . . . . . . 11
204203fveq2d 5883 . . . . . . . . . 10
205204oveq1d 6323 . . . . . . . . 9
206205oveq1d 6323 . . . . . . . 8
207206sumeq1d 13844 . . . . . . 7
208201, 207breq12d 4408 . . . . . 6
209208imbi2d 323 . . . . 5
210 oveq1 6315 . . . . . . . 8
211210oveq2d 6324 . . . . . . 7
212 oveq2 6316 . . . . . . . . . . . 12
213212oveq2d 6324 . . . . . . . . . . 11
214213fveq2d 5883 . . . . . . . . . 10
215214oveq1d 6323 . . . . . . . . 9
216215oveq1d 6323 . . . . . . . 8
217216sumeq1d 13844 . . . . . . 7
218211, 217breq12d 4408 . . . . . 6
219218imbi2d 323 . . . . 5
220 oveq1 6315 . . . . . . . 8
221220oveq2d 6324 . . . . . . 7
222 oveq2 6316 . . . . . . . . . . . 12
223222oveq2d 6324 . . . . . . . . . . 11
224223fveq2d 5883 . . . . . . . . . 10
225224oveq1d 6323 . . . . . . . . 9
226225oveq1d 6323 . . . . . . . 8
227226sumeq1d 13844 . . . . . . 7
228221, 227breq12d 4408 . . . . . 6
229228imbi2d 323 . . . . 5
23057nncnd 10647 . . . . . . . . . 10
231230subidd 9993 . . . . . . . . 9
232231oveq2d 6324 . . . . . . . 8
23352rpcnd 11366 . . . . . . . . 9
234233mul01d 9850 . . . . . . . 8
235232, 234eqtrd 2505 . . . . . . 7
236 fzfid 12224 . . . . . . . 8
23757nnzd 11062 . . . . . . . . . . . . . . . 16
23885, 237rpexpcld 12477 . . . . . . . . . . . . . . 15
23935, 238rpdivcld 11381 . . . . . . . . . . . . . 14
240239rprege0d 11371 . . . . . . . . . . . . 13
241 flge0nn0 12087 . . . . . . . . . . . . 13
242 nn0p1nn 10933 . . . . . . . . . . . . 13
243240, 241, 2423syl 18 . . . . . . . . . . . 12
244243, 181syl6eleq 2559 . . . . . . . . . . 11
245 fzss1 11863 . . . . . . . . . . 11
246244, 245syl 17 . . . . . . . . . 10
247246sselda 3418 . . . . . . . . 9
248247, 82syldan 478 . . . . . . . 8
249 elfzle2 11829 . . . . . . . . . . . . 13
250249adantl 473 . . . . . . . . . . . 12
25129simpld 466 . . . . . . . . . . . . . . 15
25235, 251rpdivcld 11381 . . . . . . . . . . . . . 14
253252rpred 11364 . . . . . . . . . . . . 13
254 elfzelz 11826 . . . . . . . . . . . . 13
255 flge 12074 . . . . . . . . . . . . 13
256253, 254, 255syl2an 485 . . . . . . . . . . . 12
257250, 256mpbird 240 . . . . . . . . . . 11
25871, 257jca 541 . . . . . . . . . 10
259 pntlem1.U . . . . . . . . . . 11
2601, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55, 259pntlemn 24517 . . . . . . . . . 10
261258, 260syldan 478 . . . . . . . . 9
262247, 261syldan 478 . . . . . . . 8
263236, 248, 262fsumge0 13932 . . . . . . 7
264235, 263eqbrtrd 4416 . . . . . 6
265264a1i 11 . . . . 5
266 pntlem1.K . . . . . . . . . 10
267 eqid 2471 . . . . . . . . . 10
2681, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55, 259, 266, 267pntlemi 24521 . . . . . . . . 9 ..^
26952adantr 472 . . . . . . . . . . 11 ..^
270269rpred 11364 . . . . . . . . . 10 ..^
271 elfzoelz 11947 . . . . . . . . . . . . . 14 ..^
272271adantl 473 . . . . . . . . . . . . 13 ..^
273272zred 11063 . . . . . . . . . . . 12 ..^
27457adantr 472 . . . . . . . . . . . . 13 ..^
275274nnred 10646 . . . . . . . . . . . 12 ..^
276273, 275resubcld 10068 . . . . . . . . . . 11 ..^
277270, 276remulcld 9689 . . . . . . . . . 10 ..^
278 fzfid 12224 . . . . . . . . . . 11 ..^
279 ssun1 3588 . . . . . . . . . . . . . . 15
28036adantr 472 . . . . . . . . . . . . . . . . . . 19 ..^
28185adantr 472 . . . . . . . . . . . . . . . . . . . 20 ..^
282272peano2zd 11066 . . . . . . . . . . . . . . . . . . . 20 ..^
283281, 282rpexpcld 12477 . . . . . . . . . . . . . . . . . . 19 ..^
284280, 283rerpdivcld 11392 . . . . . . . . . . . . . . . . . 18 ..^
285281, 272rpexpcld 12477 . . . . . . . . . . . . . . . . . . 19 ..^
286280, 285rerpdivcld 11392 . . . . . . . . . . . . . . . . . 18 ..^
28786adantr 472 . . . . . . . . . . . . . . . . . . . 20 ..^
288 1re 9660 . . . . . . . . . . . . . . . . . . . . . . 23
289 ltle 9740 . . . . . . . . . . . . . . . . . . . . . . 23
290288, 86, 289sylancr 676 . . . . . . . . . . . . . . . . . . . . . 22
29187, 290mpd 15 . . . . . . . . . . . . . . . . . . . . 21
292291adantr 472 . . . . . . . . . . . . . . . . . . . 20 ..^
293 uzid 11197 . . . . . . . . . . . . . . . . . . . . 21
294 peano2uz 11235 . . . . . . . . . . . . . . . . . . . . 21
295272, 293, 2943syl 18 . . . . . . . . . . . . . . . . . . . 20 ..^
296287, 292, 295leexp2ad 12486 . . . . . . . . . . . . . . . . . . 19 ..^
29735adantr 472 . . . . . . . . . . . . . . . . . . . 20 ..^
298285, 283, 297lediv2d 11388 . . . . . . . . . . . . . . . . . . 19 ..^
299296, 298mpbid 215 . . . . . . . . . . . . . . . . . 18 ..^
300 flword2 12081 . . . . . . . . . . . . . . . . . 18
301284, 286, 299, 300syl3anc 1292 . . . . . . . . . . . . . . . . 17 ..^
302 eluzp1p1 11208 . . . . . . . . . . . . . . . . 17
303301, 302syl 17 . . . . . . . . . . . . . . . 16 ..^
304286flcld 12067 . . . . . . . . . . . . . . . . 17 ..^
305252adantr 472 . . . . . . . . . . . . . . . . . . 19 ..^
306305rpred 11364 . . . . . . . . . . . . . . . . . 18 ..^
307306flcld 12067 . . . . . . . . . . . . . . . . 17 ..^
308251adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ..^
309308rpred 11364 . . . . . . . . . . . . . . . . . . . 20 ..^
310285rpred 11364 . . . . . . . . . . . . . . . . . . . 20 ..^
31130simpld 466 . . . . . . . . . . . . . . . . . . . . . . 23
312311rpred 11364 . . . . . . . . . . . . . . . . . . . . . 22
313312adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ..^
31430simprd 470 . . . . . . . . . . . . . . . . . . . . . 22
315314adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ..^
316 elfzofz 11962 . . . . . . . . . . . . . . . . . . . . . . 23 ..^
3171, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55pntlemh 24516 . . . . . . . . . . . . . . . . . . . . . . 23
318316, 317sylan2 482 . . . . . . . . . . . . . . . . . . . . . 22 ..^
319318simpld 466 . . . . . . . . . . . . . . . . . . . . 21 ..^
320309, 313, 310, 315, 319lttrd 9813 . . . . . . . . . . . . . . . . . . . 20 ..^
321309, 310, 320ltled 9800 . . . . . . . . . . . . . . . . . . 19 ..^
322308, 285, 297lediv2d 11388 . . . . . . . . . . . . . . . . . . 19 ..^
323321, 322mpbid 215 . . . . . . . . . . . . . . . . . 18 ..^
324 flwordi 12080 . . . . . . . . . . . . . . . . . 18
325286, 306, 323, 324syl3anc 1292 . . . . . . . . . . . . . . . . 17 ..^
326 eluz2 11188 . . . . . . . . . . . . . . . . 17
327304, 307, 325, 326syl3anbrc 1214 . . . . . . . . . . . . . . . 16 ..^
328 fzsplit2 11850 . . . . . . . . . . . . . . . 16
329303, 327, 328syl2anc 673 . . . . . . . . . . . . . . 15 ..^
330279, 329syl5sseqr 3467 . . . . . . . . . . . . . 14 ..^
331297, 283rpdivcld 11381 . . . . . . . . . . . . . . . . . 18 ..^
332331rprege0d 11371 . . . . . . . . . . . . . . . . 17 ..^
333 flge0nn0 12087 . . . . . . . . . . . . . . . . 17
334 nn0p1nn 10933 . . . . . . . . . . . . . . . . 17
335332, 333, 3343syl 18 . . . . . . . . . . . . . . . 16 ..^
336335, 181syl6eleq 2559 . . . . . . . . . . . . . . 15 ..^
337 fzss1 11863 . . . . . . . . . . . . . . 15
338336, 337syl 17 . . . . . . . . . . . . . 14 ..^
339330, 338sstrd 3428 . . . . . . . . . . . . 13 ..^
340339sselda 3418 . . . . . . . . . . . 12 ..^
34182adantlr 729 . . . . . . . . . . . 12 ..^
342340, 341syldan 478 . . . . . . . . . . 11 ..^
343278, 342fsumrecl 13877 . . . . . . . . . 10 ..^
344 fzfid 12224 . . . . . . . . . . 11 ..^
345 ssun2 3589 . . . . . . . . . . . . . . 15
346345, 329syl5sseqr 3467 . . . . . . . . . . . . . 14 ..^
347346, 338sstrd 3428 . . . . . . . . . . . . 13 ..^
348347sselda 3418 . . . . . . . . . . . 12 ..^
349348, 341syldan 478 . . . . . . . . . . 11 ..^
350344, 349fsumrecl 13877 . . . . . . . . . 10 ..^
351 le2add 10117 . . . . . . . . . 10
352270, 277, 343, 350, 351syl22anc 1293 . . . . . . . . 9 ..^
353268, 352mpand 689 . . . . . . . 8 ..^