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

Theorem pntlemo 24524
 Description: Lemma for pnt 24531. Combine all the estimates to establish a smaller eventual bound on . (Contributed by Mario Carneiro, 14-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
pntlem1.C
Assertion
Ref Expression
pntlemo
Distinct variable groups:   ,   ,,,   ,,   ,   ,   ,,,,   ,   ,   ,,   ,,   ,,,,   ,,
Allowed substitution hints:   (,,,,)   (,,,,)   (,,,,)   (,,,)   (,,,,)   ()   (,,,)   ()   (,,,,)   (,,)   (,)   (,,,)   (,,,)   (,,,)   (,,)   (,,)   (,,)

Proof of Theorem pntlemo
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 pntlem1.r . . . . . . . . . 10 ψ
2 pntlem1.a . . . . . . . . . 10
3 pntlem1.b . . . . . . . . . 10
4 pntlem1.l . . . . . . . . . 10
5 pntlem1.d . . . . . . . . . 10
6 pntlem1.f . . . . . . . . . 10 ;
7 pntlem1.u . . . . . . . . . 10
8 pntlem1.u2 . . . . . . . . . 10
9 pntlem1.e . . . . . . . . . 10
10 pntlem1.k . . . . . . . . . 10
11 pntlem1.y . . . . . . . . . 10
12 pntlem1.x . . . . . . . . . 10
13 pntlem1.c . . . . . . . . . 10
14 pntlem1.w . . . . . . . . . 10 ;
15 pntlem1.z . . . . . . . . . 10
161, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15pntlemb 24514 . . . . . . . . 9 ;
1716simp1d 1042 . . . . . . . 8
181pntrf 24480 . . . . . . . . 9
1918ffvelrni 6036 . . . . . . . 8
2017, 19syl 17 . . . . . . 7
2120, 17rerpdivcld 11392 . . . . . 6
2221recnd 9687 . . . . 5
2322abscld 13575 . . . 4
2417relogcld 23651 . . . 4
2523, 24remulcld 9689 . . 3
267rpred 11364 . . . . . 6
27 3re 10705 . . . . . . . 8
2827a1i 11 . . . . . . 7
2924, 28readdcld 9688 . . . . . 6
3026, 29remulcld 9689 . . . . 5
31 2re 10701 . . . . . . 7
3231a1i 11 . . . . . 6
331, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 24512 . . . . . . . . . . 11
3433simp3d 1044 . . . . . . . . . 10
3534simp3d 1044 . . . . . . . . 9
3635rpred 11364 . . . . . . . 8
371, 2, 3, 4, 5, 6pntlemd 24511 . . . . . . . . . . . 12
3837simp1d 1042 . . . . . . . . . . 11
3933simp1d 1042 . . . . . . . . . . . 12
40 2z 10993 . . . . . . . . . . . 12
41 rpexpcl 12329 . . . . . . . . . . . 12
4239, 40, 41sylancl 675 . . . . . . . . . . 11
4338, 42rpmulcld 11380 . . . . . . . . . 10
44 3nn0 10911 . . . . . . . . . . . . 13
45 2nn 10790 . . . . . . . . . . . . 13
4644, 45decnncl 11087 . . . . . . . . . . . 12 ;
47 nnrp 11334 . . . . . . . . . . . 12 ; ;
4846, 47ax-mp 5 . . . . . . . . . . 11 ;
49 rpmulcl 11347 . . . . . . . . . . 11 ; ;
5048, 3, 49sylancr 676 . . . . . . . . . 10 ;
5143, 50rpdivcld 11381 . . . . . . . . 9 ;
5251rpred 11364 . . . . . . . 8 ;
5336, 52remulcld 9689 . . . . . . 7 ;
5453, 24remulcld 9689 . . . . . 6 ;
5532, 54remulcld 9689 . . . . 5 ;
5630, 55resubcld 10068 . . . 4 ;
5713rpred 11364 . . . 4
5856, 57readdcld 9688 . . 3 ;
597rpcnd 11366 . . . . . 6
6053recnd 9687 . . . . . 6 ;
6124recnd 9687 . . . . . 6
6259, 60, 61subdird 10096 . . . . 5 ; ;
6338rpcnd 11366 . . . . . . . . . . 11
6442rpcnd 11366 . . . . . . . . . . 11
6550rpcnne0d 11373 . . . . . . . . . . 11 ; ;
66 div23 10311 . . . . . . . . . . 11 ; ; ; ;
6763, 64, 65, 66syl3anc 1292 . . . . . . . . . 10 ; ;
689oveq1i 6318 . . . . . . . . . . . 12
6937simp2d 1043 . . . . . . . . . . . . . 14
7069rpcnd 11366 . . . . . . . . . . . . 13
7169rpne0d 11369 . . . . . . . . . . . . 13
7259, 70, 71sqdivd 12467 . . . . . . . . . . . 12
7368, 72syl5eq 2517 . . . . . . . . . . 11
7473oveq2d 6324 . . . . . . . . . 10 ; ;
7538, 50rpdivcld 11381 . . . . . . . . . . . 12 ;
7675rpcnd 11366 . . . . . . . . . . 11 ;
7759sqcld 12452 . . . . . . . . . . 11
78 rpexpcl 12329 . . . . . . . . . . . . 13
7969, 40, 78sylancl 675 . . . . . . . . . . . 12
8079rpcnne0d 11373 . . . . . . . . . . 11
81 divass 10310 . . . . . . . . . . . 12 ; ; ;
82 div23 10311 . . . . . . . . . . . 12 ; ; ;
8381, 82eqtr3d 2507 . . . . . . . . . . 11 ; ; ;
8476, 77, 80, 83syl3anc 1292 . . . . . . . . . 10 ; ;
8567, 74, 843eqtrd 2509 . . . . . . . . 9 ; ;
8685oveq2d 6324 . . . . . . . 8 ; ;
87 df-3 10691 . . . . . . . . . . . . 13
8887oveq2i 6319 . . . . . . . . . . . 12
89 2nn0 10910 . . . . . . . . . . . . 13
90 expp1 12317 . . . . . . . . . . . . 13
9159, 89, 90sylancl 675 . . . . . . . . . . . 12
9288, 91syl5eq 2517 . . . . . . . . . . 11
9377, 59mulcomd 9682 . . . . . . . . . . 11
9492, 93eqtrd 2505 . . . . . . . . . 10
9594oveq2d 6324 . . . . . . . . 9
9637simp3d 1044 . . . . . . . . . . 11
9796rpcnd 11366 . . . . . . . . . 10
9897, 59, 77mulassd 9684 . . . . . . . . 9
99 1cnd 9677 . . . . . . . . . . . . . . 15
10069rpreccld 11374 . . . . . . . . . . . . . . . 16
101100rpcnd 11366 . . . . . . . . . . . . . . 15
10299, 101, 59subdird 10096 . . . . . . . . . . . . . 14
10359mulid2d 9679 . . . . . . . . . . . . . . 15
10459, 70, 71divrec2d 10409 . . . . . . . . . . . . . . . 16
1059, 104syl5req 2518 . . . . . . . . . . . . . . 15
106103, 105oveq12d 6326 . . . . . . . . . . . . . 14
107102, 106eqtr2d 2506 . . . . . . . . . . . . 13
108107oveq1d 6323 . . . . . . . . . . . 12 ; ;
1096oveq1i 6318 . . . . . . . . . . . . 13 ;
11099, 101subcld 10005 . . . . . . . . . . . . . 14
11175, 79rpdivcld 11381 . . . . . . . . . . . . . . 15 ;
112111rpcnd 11366 . . . . . . . . . . . . . 14 ;
113110, 112, 59mul32d 9861 . . . . . . . . . . . . 13 ; ;
114109, 113syl5eq 2517 . . . . . . . . . . . 12 ;
115108, 114eqtr4d 2508 . . . . . . . . . . 11 ;
116115oveq1d 6323 . . . . . . . . . 10 ;
11735rpcnd 11366 . . . . . . . . . . 11
118117, 112, 77mulassd 9684 . . . . . . . . . 10 ; ;
119116, 118eqtr3d 2507 . . . . . . . . 9 ;
12095, 98, 1193eqtr2d 2511 . . . . . . . 8 ;
12186, 120eqtr4d 2508 . . . . . . 7 ;
122121oveq2d 6324 . . . . . 6 ;
123122oveq1d 6323 . . . . 5 ;
12462, 123eqtr3d 2507 . . . 4 ;
12526, 24remulcld 9689 . . . . 5
126125, 54resubcld 10068 . . . 4 ;
127124, 126eqeltrrd 2550 . . 3
12817rpred 11364 . . . . . . . 8
12916simp2d 1043 . . . . . . . . 9
130129simp1d 1042 . . . . . . . 8
131128, 130rplogcld 23657 . . . . . . 7
13232, 131rerpdivcld 11392 . . . . . 6
133 fzfid 12224 . . . . . . 7
13417adantr 472 . . . . . . . . . . . . 13
135 elfznn 11854 . . . . . . . . . . . . . . 15
136135adantl 473 . . . . . . . . . . . . . 14
137136nnrpd 11362 . . . . . . . . . . . . 13
138134, 137rpdivcld 11381 . . . . . . . . . . . 12
13918ffvelrni 6036 . . . . . . . . . . . 12
140138, 139syl 17 . . . . . . . . . . 11
141140, 134rerpdivcld 11392 . . . . . . . . . 10
142141recnd 9687 . . . . . . . . 9
143142abscld 13575 . . . . . . . 8
144137relogcld 23651 . . . . . . . 8
145143, 144remulcld 9689 . . . . . . 7
146133, 145fsumrecl 13877 . . . . . 6
147132, 146remulcld 9689 . . . . 5
148147, 57readdcld 9688 . . . 4
14920recnd 9687 . . . . . . . . . . 11
150149abscld 13575 . . . . . . . . . 10
151150recnd 9687 . . . . . . . . 9
152151, 61mulcld 9681 . . . . . . . 8
153132recnd 9687 . . . . . . . . 9
154140recnd 9687 . . . . . . . . . . . . 13
155154abscld 13575 . . . . . . . . . . . 12
156155, 144remulcld 9689 . . . . . . . . . . 11
157133, 156fsumrecl 13877 . . . . . . . . . 10
158157recnd 9687 . . . . . . . . 9
159153, 158mulcld 9681 . . . . . . . 8
16017rpcnd 11366 . . . . . . . 8
16117rpne0d 11369 . . . . . . . 8
162152, 159, 160, 161divsubdird 10444 . . . . . . 7
163151, 61, 160, 161div23d 10442 . . . . . . . . 9
164149, 160, 161absdivd 13594 . . . . . . . . . . 11
16517rprege0d 11371 . . . . . . . . . . . . 13
166 absid 13436 . . . . . . . . . . . . 13
167165, 166syl 17 . . . . . . . . . . . 12
168167oveq2d 6324 . . . . . . . . . . 11
169164, 168eqtrd 2505 . . . . . . . . . 10
170169oveq1d 6323 . . . . . . . . 9
171163, 170eqtr4d 2508 . . . . . . . 8
172153, 158, 160, 161divassd 10440 . . . . . . . . 9
173160adantr 472 . . . . . . . . . . . . . . . 16
174161adantr 472 . . . . . . . . . . . . . . . 16
175154, 173, 174absdivd 13594 . . . . . . . . . . . . . . 15
176167adantr 472 . . . . . . . . . . . . . . . 16
177176oveq2d 6324 . . . . . . . . . . . . . . 15
178175, 177eqtrd 2505 . . . . . . . . . . . . . 14
179178oveq1d 6323 . . . . . . . . . . . . 13
180155recnd 9687 . . . . . . . . . . . . . 14
181144recnd 9687 . . . . . . . . . . . . . 14
18217rpcnne0d 11373 . . . . . . . . . . . . . . 15
183182adantr 472 . . . . . . . . . . . . . 14
184 div23 10311 . . . . . . . . . . . . . 14
185180, 181, 183, 184syl3anc 1292 . . . . . . . . . . . . 13
186179, 185eqtr4d 2508 . . . . . . . . . . . 12
187186sumeq2dv 13846 . . . . . . . . . . 11
188156recnd 9687 . . . . . . . . . . . 12
189133, 160, 188, 161fsumdivc 13924 . . . . . . . . . . 11
190187, 189eqtr4d 2508 . . . . . . . . . 10
191190oveq2d 6324 . . . . . . . . 9
192172, 191eqtr4d 2508 . . . . . . . 8
193171, 192oveq12d 6326 . . . . . . 7
194162, 193eqtrd 2505 . . . . . 6
195 1re 9660 . . . . . . . . 9
196 rexr 9704 . . . . . . . . 9
197 elioopnf 11753 . . . . . . . . 9
198195, 196, 197mp2b 10 . . . . . . . 8
199128, 130, 198sylanbrc 677 . . . . . . 7
200 pntlem1.C . . . . . . 7
201 fveq2 5879 . . . . . . . . . . . . 13
202201fveq2d 5883 . . . . . . . . . . . 12
203 fveq2 5879 . . . . . . . . . . . 12
204202, 203oveq12d 6326 . . . . . . . . . . 11
205203oveq2d 6324 . . . . . . . . . . . 12
206 oveq2 6316 . . . . . . . . . . . . . . . . 17
207206fveq2d 5883 . . . . . . . . . . . . . . . 16
208207fveq2d 5883 . . . . . . . . . . . . . . 15
209 fveq2 5879 . . . . . . . . . . . . . . 15
210208, 209oveq12d 6326 . . . . . . . . . . . . . 14
211210cbvsumv 13839 . . . . . . . . . . . . 13
212 oveq1 6315 . . . . . . . . . . . . . . . 16
213212fveq2d 5883 . . . . . . . . . . . . . . 15
214213oveq2d 6324 . . . . . . . . . . . . . 14
215 simpl 464 . . . . . . . . . . . . . . . . . 18
216215oveq1d 6323 . . . . . . . . . . . . . . . . 17
217216fveq2d 5883 . . . . . . . . . . . . . . . 16
218217fveq2d 5883 . . . . . . . . . . . . . . 15
219218oveq1d 6323 . . . . . . . . . . . . . 14
220214, 219sumeq12rdv 13850 . . . . . . . . . . . . 13
221211, 220syl5eq 2517 . . . . . . . . . . . 12
222205, 221oveq12d 6326 . . . . . . . . . . 11
223204, 222oveq12d 6326 . . . . . . . . . 10
224 id 22 . . . . . . . . . 10
225223, 224oveq12d 6326 . . . . . . . . 9
226225breq1d 4405 . . . . . . . 8
227226rspcv 3132 . . . . . . 7
228199, 200, 227sylc 61 . . . . . 6
229194, 228eqbrtrrd 4418 . . . . 5
23025, 147, 57lesubadd2d 10233 . . . . 5
231229, 230mpbid 215 . . . 4
232 2cnd 10704 . . . . . . 7
233143recnd 9687 . . . . . . . . 9
234233, 181mulcld 9681 . . . . . . . 8
235133, 234fsumcl 13876 . . . . . . 7
236131rpne0d 11369 . . . . . . 7
237232, 235, 61, 236div23d 10442 . . . . . 6
23824resqcld 12480 . . . . . . . . . . . 12
23952, 238remulcld 9689 . . . . . . . . . . 11 ;
24036, 239remulcld 9689 . . . . . . . . . 10 ;
241 remulcl 9642 . . . . . . . . . 10 ; ;
24231, 240, 241sylancr 676 . . . . . . . . 9 ;
24330, 24remulcld 9689 . . . . . . . . 9
244 remulcl 9642 . . . . . . . . . 10
24531, 146, 244sylancr 676 . . . . . . . . 9
24626adantr 472 . . . . . . . . . . . . . . 15
247246, 136nndivred 10680 . . . . . . . . . . . . . 14
248247, 143resubcld 10068 . . . . . . . . . . . . 13
249248, 144remulcld 9689 . . . . . . . . . . . 12
250133, 249fsumrecl 13877 . . . . . . . . . . 11
25132, 250remulcld 9689 . . . . . . . . . 10
252243, 245resubcld 10068 . . . . . . . . . 10
253 pntlem1.m . . . . . . . . . . . 12
254 pntlem1.n . . . . . . . . . . . 12
255 pntlem1.U . . . . . . . . . . . 12
256 pntlem1.K . . . . . . . . . . . 12
2571, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 253, 254, 255, 256pntlemf 24522 . . . . . . . . . . 11 ;
258 2pos 10723 . . . . . . . . . . . . 13
259258a1i 11 . . . . . . . . . . . 12
260 lemul2 10480 . . . . . . . . . . . 12 ; ; ;
261240, 250, 32, 259, 260syl112anc 1296 . . . . . . . . . . 11 ; ;
262257, 261mpbid 215 . . . . . . . . . 10 ;
263247recnd 9687 . . . . . . . . . . . . . . . 16
264263, 233, 181subdird 10096 . . . . . . . . . . . . . . 15
265264sumeq2dv 13846 . . . . . . . . . . . . . 14
266247, 144remulcld 9689 . . . . . . . . . . . . . . . 16
267266recnd 9687 . . . . . . . . . . . . . . 15
268133, 267, 234fsumsub 13926 . . . . . . . . . . . . . 14
269265, 268eqtrd 2505 . . . . . . . . . . . . 13
270269oveq2d 6324 . . . . . . . . . . . 12
271133, 266fsumrecl 13877 . . . . . . . . . . . . . 14
272271recnd 9687 . . . . . . . . . . . . 13
273232, 272, 235subdid 10095 . . . . . . . . . . . 12
274270, 273eqtrd 2505 . . . . . . . . . . 11
275 remulcl 9642 . . . . . . . . . . . . 13
27631, 271, 275sylancr 676 . . . . . . . . . . . 12
2771, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 253, 254, 255, 256pntlemk 24523 . . . . . . . . . . . 12
278276, 243, 245, 277lesub1dd 10250 . . . . . . . . . . 11
279274, 278eqbrtrd 4416 . . . . . . . . . 10
280242, 251, 252, 262, 279letrd 9809 . . . . . . . . 9 ;
281242, 243, 245, 280lesubd 10238 . . . . . . . 8 ;
28230recnd 9687 . . . . . . . . . 10
28355recnd 9687 . . . . . . . . . 10 ;
284282, 283, 61subdird 10096 . . . . . . . . 9 ; ;
28554recnd 9687 . . . . . . . . . . . 12 ;
286232, 285, 61mulassd 9684 . . . . . . . . . . 11 ; ;
28760, 61, 61mulassd 9684 . . . . . . . . . . . . 13 ; ;
28861sqvald 12451 . . . . . . . . . . . . . 14
289288oveq2d 6324 . . . . . . . . . . . . 13 ; ;
29051rpcnd 11366 . . . . . . . . . . . . . 14 ;
291238recnd 9687 . . . . . . . . . . . . . 14
292117, 290, 291mulassd 9684 . . . . . . . . . . . . 13 ; ;
293287, 289, 2923eqtr2d 2511 . . . . . . . . . . . 12 ; ;
294293oveq2d 6324 . . . . . . . . . . 11 ; ;
295286, 294eqtrd 2505 . . . . . . . . . 10 ; ;
296295oveq2d 6324 . . . . . . . . 9 ; ;
297284, 296eqtrd 2505 . . . . . . . 8 ; ;
298281, 297breqtrrd 4422 . . . . . . 7 ;
299245, 56, 131ledivmul2d 11415 . . . . . . 7 ; ;
300298, 299mpbird 240 . . . . . 6 ;
301237, 300eqbrtrrd 4418 . . . . 5 ;
302147, 56, 57, 301leadd1dd 10248 . . . 4 ;
30325, 148, 58, 231, 302letrd 9809 . . 3 ;
304 remulcl 9642 . . . . . . . . 9
30526, 27, 304sylancl 675 . . . . . . . 8
306305, 57readdcld 9688 . . . . . . 7
30716simp3d 1044 . . . . . . . 8 ;
308307simp3d 1044 . . . . . . 7 ;
309306, 54, 125, 308leadd2dd 10249 . . . . . 6 ;
31028recnd 9687 . . . . . . . . 9
31159, 61, 310adddid 9685 . . . . . . . 8
312311oveq1d 6323 . . . . . . 7
313125recnd 9687 . . . . . . . 8
31459, 310mulcld 9681 . . . . . . . 8
31513rpcnd 11366 . . . . . . . 8
316313, 314, 315addassd 9683 . . . . . . 7
317312, 316eqtrd 2505 . . . . . 6
3182852timesd 10878 . . . . . . . 8 ; ; ;
319318oveq2d 6324 . . . . . . 7 ; ; ; ; ;
320313, 285, 285nppcan3d 10032 . . . . . . 7 ; ; ; ;
321319, 320eqtrd 2505 . . . . . 6 ; ; ;
322309, 317, 3213brtr4d 4426 . . . . 5 ;