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

Theorem pntlemo 21254
 Description: Lemma for pnt 21261. 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 21244 . . . . . . . . 9 ;
1716simp1d 969 . . . . . . . 8
181pntrf 21210 . . . . . . . . 9
1918ffvelrni 5828 . . . . . . . 8
2017, 19syl 16 . . . . . . 7
2120, 17rerpdivcld 10631 . . . . . 6
2221recnd 9070 . . . . 5
2322abscld 12193 . . . 4
2417relogcld 20471 . . . 4
2523, 24remulcld 9072 . . 3
267rpred 10604 . . . . . 6
27 3re 10027 . . . . . . . 8
2827a1i 11 . . . . . . 7
2924, 28readdcld 9071 . . . . . 6
3026, 29remulcld 9072 . . . . 5
31 2re 10025 . . . . . . 7
3231a1i 11 . . . . . 6
331, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 21242 . . . . . . . . . . 11
3433simp3d 971 . . . . . . . . . 10
3534simp3d 971 . . . . . . . . 9
3635rpred 10604 . . . . . . . 8
371, 2, 3, 4, 5, 6pntlemd 21241 . . . . . . . . . . . 12
3837simp1d 969 . . . . . . . . . . 11
3933simp1d 969 . . . . . . . . . . . 12
40 2z 10268 . . . . . . . . . . . 12
41 rpexpcl 11355 . . . . . . . . . . . 12
4239, 40, 41sylancl 644 . . . . . . . . . . 11
4338, 42rpmulcld 10620 . . . . . . . . . 10
44 3nn0 10195 . . . . . . . . . . . . 13
45 2nn 10089 . . . . . . . . . . . . 13
4644, 45decnncl 10351 . . . . . . . . . . . 12 ;
47 nnrp 10577 . . . . . . . . . . . 12 ; ;
4846, 47ax-mp 8 . . . . . . . . . . 11 ;
49 rpmulcl 10589 . . . . . . . . . . 11 ; ;
5048, 3, 49sylancr 645 . . . . . . . . . 10 ;
5143, 50rpdivcld 10621 . . . . . . . . 9 ;
5251rpred 10604 . . . . . . . 8 ;
5336, 52remulcld 9072 . . . . . . 7 ;
5453, 24remulcld 9072 . . . . . 6 ;
5532, 54remulcld 9072 . . . . 5 ;
5630, 55resubcld 9421 . . . 4 ;
5713rpred 10604 . . . 4
5856, 57readdcld 9071 . . 3 ;
597rpcnd 10606 . . . . . 6
6053recnd 9070 . . . . . 6 ;
6124recnd 9070 . . . . . 6
6259, 60, 61subdird 9446 . . . . 5 ; ;
6338rpcnd 10606 . . . . . . . . . . 11
6442rpcnd 10606 . . . . . . . . . . 11
6550rpcnne0d 10613 . . . . . . . . . . 11 ; ;
66 div23 9653 . . . . . . . . . . 11 ; ; ; ;
6763, 64, 65, 66syl3anc 1184 . . . . . . . . . 10 ; ;
689oveq1i 6050 . . . . . . . . . . . 12
6937simp2d 970 . . . . . . . . . . . . . 14
7069rpcnd 10606 . . . . . . . . . . . . 13
7169rpne0d 10609 . . . . . . . . . . . . 13
7259, 70, 71sqdivd 11491 . . . . . . . . . . . 12
7368, 72syl5eq 2448 . . . . . . . . . . 11
7473oveq2d 6056 . . . . . . . . . 10 ; ;
7538, 50rpdivcld 10621 . . . . . . . . . . . 12 ;
7675rpcnd 10606 . . . . . . . . . . 11 ;
7759sqcld 11476 . . . . . . . . . . 11
78 rpexpcl 11355 . . . . . . . . . . . . 13
7969, 40, 78sylancl 644 . . . . . . . . . . . 12
8079rpcnne0d 10613 . . . . . . . . . . 11
81 divass 9652 . . . . . . . . . . . 12 ; ; ;
82 div23 9653 . . . . . . . . . . . 12 ; ; ;
8381, 82eqtr3d 2438 . . . . . . . . . . 11 ; ; ;
8476, 77, 80, 83syl3anc 1184 . . . . . . . . . 10 ; ;
8567, 74, 843eqtrd 2440 . . . . . . . . 9 ; ;
8685oveq2d 6056 . . . . . . . 8 ; ;
87 df-3 10015 . . . . . . . . . . . . 13
8887oveq2i 6051 . . . . . . . . . . . 12
89 2nn0 10194 . . . . . . . . . . . . 13
90 expp1 11343 . . . . . . . . . . . . 13
9159, 89, 90sylancl 644 . . . . . . . . . . . 12
9288, 91syl5eq 2448 . . . . . . . . . . 11
9377, 59mulcomd 9065 . . . . . . . . . . 11
9492, 93eqtrd 2436 . . . . . . . . . 10
9594oveq2d 6056 . . . . . . . . 9
9637simp3d 971 . . . . . . . . . . 11
9796rpcnd 10606 . . . . . . . . . 10
9897, 59, 77mulassd 9067 . . . . . . . . 9
99 ax-1cn 9004 . . . . . . . . . . . . . . . 16
10099a1i 11 . . . . . . . . . . . . . . 15
10169rpreccld 10614 . . . . . . . . . . . . . . . 16
102101rpcnd 10606 . . . . . . . . . . . . . . 15
103100, 102, 59subdird 9446 . . . . . . . . . . . . . 14
10459mulid2d 9062 . . . . . . . . . . . . . . 15
10559, 70, 71divrec2d 9750 . . . . . . . . . . . . . . . 16
1069, 105syl5req 2449 . . . . . . . . . . . . . . 15
107104, 106oveq12d 6058 . . . . . . . . . . . . . 14
108103, 107eqtr2d 2437 . . . . . . . . . . . . 13
109108oveq1d 6055 . . . . . . . . . . . 12 ; ;
1106oveq1i 6050 . . . . . . . . . . . . 13 ;
111100, 102subcld 9367 . . . . . . . . . . . . . 14
11275, 79rpdivcld 10621 . . . . . . . . . . . . . . 15 ;
113112rpcnd 10606 . . . . . . . . . . . . . 14 ;
114111, 113, 59mul32d 9232 . . . . . . . . . . . . 13 ; ;
115110, 114syl5eq 2448 . . . . . . . . . . . 12 ;
116109, 115eqtr4d 2439 . . . . . . . . . . 11 ;
117116oveq1d 6055 . . . . . . . . . 10 ;
11835rpcnd 10606 . . . . . . . . . . 11
119118, 113, 77mulassd 9067 . . . . . . . . . 10 ; ;
120117, 119eqtr3d 2438 . . . . . . . . 9 ;
12195, 98, 1203eqtr2d 2442 . . . . . . . 8 ;
12286, 121eqtr4d 2439 . . . . . . 7 ;
123122oveq2d 6056 . . . . . 6 ;
124123oveq1d 6055 . . . . 5 ;
12562, 124eqtr3d 2438 . . . 4 ;
12626, 24remulcld 9072 . . . . 5
127126, 54resubcld 9421 . . . 4 ;
128125, 127eqeltrrd 2479 . . 3
12917rpred 10604 . . . . . . . 8
13016simp2d 970 . . . . . . . . 9
131130simp1d 969 . . . . . . . 8
132129, 131rplogcld 20477 . . . . . . 7
13332, 132rerpdivcld 10631 . . . . . 6
134 fzfid 11267 . . . . . . 7
13517adantr 452 . . . . . . . . . . . . 13
136 elfznn 11036 . . . . . . . . . . . . . . 15
137136adantl 453 . . . . . . . . . . . . . 14
138137nnrpd 10603 . . . . . . . . . . . . 13
139135, 138rpdivcld 10621 . . . . . . . . . . . 12
14018ffvelrni 5828 . . . . . . . . . . . 12
141139, 140syl 16 . . . . . . . . . . 11
142141, 135rerpdivcld 10631 . . . . . . . . . 10
143142recnd 9070 . . . . . . . . 9
144143abscld 12193 . . . . . . . 8
145138relogcld 20471 . . . . . . . 8
146144, 145remulcld 9072 . . . . . . 7
147134, 146fsumrecl 12483 . . . . . 6
148133, 147remulcld 9072 . . . . 5
149148, 57readdcld 9071 . . . 4
15020recnd 9070 . . . . . . . . . . 11
151150abscld 12193 . . . . . . . . . 10
152151recnd 9070 . . . . . . . . 9
153152, 61mulcld 9064 . . . . . . . 8
154133recnd 9070 . . . . . . . . 9
155141recnd 9070 . . . . . . . . . . . . 13
156155abscld 12193 . . . . . . . . . . . 12
157156, 145remulcld 9072 . . . . . . . . . . 11
158134, 157fsumrecl 12483 . . . . . . . . . 10
159158recnd 9070 . . . . . . . . 9
160154, 159mulcld 9064 . . . . . . . 8
16117rpcnd 10606 . . . . . . . 8
16217rpne0d 10609 . . . . . . . 8
163153, 160, 161, 162divsubdird 9785 . . . . . . 7
164152, 61, 161, 162div23d 9783 . . . . . . . . 9
165150, 161, 162absdivd 12212 . . . . . . . . . . 11
16617rprege0d 10611 . . . . . . . . . . . . 13
167 absid 12056 . . . . . . . . . . . . 13
168166, 167syl 16 . . . . . . . . . . . 12
169168oveq2d 6056 . . . . . . . . . . 11
170165, 169eqtrd 2436 . . . . . . . . . 10
171170oveq1d 6055 . . . . . . . . 9
172164, 171eqtr4d 2439 . . . . . . . 8
173154, 159, 161, 162divassd 9781 . . . . . . . . 9
174161adantr 452 . . . . . . . . . . . . . . . 16
175162adantr 452 . . . . . . . . . . . . . . . 16
176155, 174, 175absdivd 12212 . . . . . . . . . . . . . . 15
177168adantr 452 . . . . . . . . . . . . . . . 16
178177oveq2d 6056 . . . . . . . . . . . . . . 15
179176, 178eqtrd 2436 . . . . . . . . . . . . . 14
180179oveq1d 6055 . . . . . . . . . . . . 13
181156recnd 9070 . . . . . . . . . . . . . 14
182145recnd 9070 . . . . . . . . . . . . . 14
18317rpcnne0d 10613 . . . . . . . . . . . . . . 15
184183adantr 452 . . . . . . . . . . . . . 14
185 div23 9653 . . . . . . . . . . . . . 14
186181, 182, 184, 185syl3anc 1184 . . . . . . . . . . . . 13
187180, 186eqtr4d 2439 . . . . . . . . . . . 12
188187sumeq2dv 12452 . . . . . . . . . . 11
189157recnd 9070 . . . . . . . . . . . 12
190134, 161, 189, 162fsumdivc 12524 . . . . . . . . . . 11
191188, 190eqtr4d 2439 . . . . . . . . . 10
192191oveq2d 6056 . . . . . . . . 9
193173, 192eqtr4d 2439 . . . . . . . 8
194172, 193oveq12d 6058 . . . . . . 7
195163, 194eqtrd 2436 . . . . . 6
196 1re 9046 . . . . . . . . 9
197 rexr 9086 . . . . . . . . 9
198 elioopnf 10954 . . . . . . . . 9
199196, 197, 198mp2b 10 . . . . . . . 8
200129, 131, 199sylanbrc 646 . . . . . . 7
201 pntlem1.C . . . . . . 7
202 fveq2 5687 . . . . . . . . . . . . 13
203202fveq2d 5691 . . . . . . . . . . . 12
204 fveq2 5687 . . . . . . . . . . . 12
205203, 204oveq12d 6058 . . . . . . . . . . 11
206204oveq2d 6056 . . . . . . . . . . . 12
207 oveq2 6048 . . . . . . . . . . . . . . . . 17
208207fveq2d 5691 . . . . . . . . . . . . . . . 16
209208fveq2d 5691 . . . . . . . . . . . . . . 15
210 fveq2 5687 . . . . . . . . . . . . . . 15
211209, 210oveq12d 6058 . . . . . . . . . . . . . 14
212211cbvsumv 12445 . . . . . . . . . . . . 13
213 oveq1 6047 . . . . . . . . . . . . . . . 16
214213fveq2d 5691 . . . . . . . . . . . . . . 15
215214oveq2d 6056 . . . . . . . . . . . . . 14
216 simpl 444 . . . . . . . . . . . . . . . . . 18
217216oveq1d 6055 . . . . . . . . . . . . . . . . 17
218217fveq2d 5691 . . . . . . . . . . . . . . . 16
219218fveq2d 5691 . . . . . . . . . . . . . . 15
220219oveq1d 6055 . . . . . . . . . . . . . 14
221215, 220sumeq12rdv 12456 . . . . . . . . . . . . 13
222212, 221syl5eq 2448 . . . . . . . . . . . 12
223206, 222oveq12d 6058 . . . . . . . . . . 11
224205, 223oveq12d 6058 . . . . . . . . . 10
225 id 20 . . . . . . . . . 10
226224, 225oveq12d 6058 . . . . . . . . 9
227226breq1d 4182 . . . . . . . 8
228227rspcv 3008 . . . . . . 7
229200, 201, 228sylc 58 . . . . . 6
230195, 229eqbrtrrd 4194 . . . . 5
23125, 148, 57lesubadd2d 9581 . . . . 5
232230, 231mpbid 202 . . . 4
233 2cn 10026 . . . . . . . 8
234233a1i 11 . . . . . . 7
235144recnd 9070 . . . . . . . . 9
236235, 182mulcld 9064 . . . . . . . 8
237134, 236fsumcl 12482 . . . . . . 7
238132rpne0d 10609 . . . . . . 7
239234, 237, 61, 238div23d 9783 . . . . . 6
24024resqcld 11504 . . . . . . . . . . . 12
24152, 240remulcld 9072 . . . . . . . . . . 11 ;
24236, 241remulcld 9072 . . . . . . . . . 10 ;
243 remulcl 9031 . . . . . . . . . 10 ; ;
24431, 242, 243sylancr 645 . . . . . . . . 9 ;
24530, 24remulcld 9072 . . . . . . . . 9
246 remulcl 9031 . . . . . . . . . 10
24731, 147, 246sylancr 645 . . . . . . . . 9
24826adantr 452 . . . . . . . . . . . . . . 15
249248, 137nndivred 10004 . . . . . . . . . . . . . 14
250249, 144resubcld 9421 . . . . . . . . . . . . 13
251250, 145remulcld 9072 . . . . . . . . . . . 12
252134, 251fsumrecl 12483 . . . . . . . . . . 11
25332, 252remulcld 9072 . . . . . . . . . 10
254245, 247resubcld 9421 . . . . . . . . . 10
255 pntlem1.m . . . . . . . . . . . 12
256 pntlem1.n . . . . . . . . . . . 12
257 pntlem1.U . . . . . . . . . . . 12
258 pntlem1.K . . . . . . . . . . . 12
2591, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 255, 256, 257, 258pntlemf 21252 . . . . . . . . . . 11 ;
260 2pos 10038 . . . . . . . . . . . . 13
261260a1i 11 . . . . . . . . . . . 12
262 lemul2 9819 . . . . . . . . . . . 12 ; ; ;
263242, 252, 32, 261, 262syl112anc 1188 . . . . . . . . . . 11 ; ;
264259, 263mpbid 202 . . . . . . . . . 10 ;
265249recnd 9070 . . . . . . . . . . . . . . . 16
266265, 235, 182subdird 9446 . . . . . . . . . . . . . . 15
267266sumeq2dv 12452 . . . . . . . . . . . . . 14
268249, 145remulcld 9072 . . . . . . . . . . . . . . . 16
269268recnd 9070 . . . . . . . . . . . . . . 15
270134, 269, 236fsumsub 12526 . . . . . . . . . . . . . 14
271267, 270eqtrd 2436 . . . . . . . . . . . . 13
272271oveq2d 6056 . . . . . . . . . . . 12
273134, 268fsumrecl 12483 . . . . . . . . . . . . . 14
274273recnd 9070 . . . . . . . . . . . . 13
275234, 274, 237subdid 9445 . . . . . . . . . . . 12
276272, 275eqtrd 2436 . . . . . . . . . . 11
277 remulcl 9031 . . . . . . . . . . . . 13
27831, 273, 277sylancr 645 . . . . . . . . . . . 12
2791, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 255, 256, 257, 258pntlemk 21253 . . . . . . . . . . . 12
280278, 245, 247, 279lesub1dd 9598 . . . . . . . . . . 11
281276, 280eqbrtrd 4192 . . . . . . . . . 10
282244, 253, 254, 264, 281letrd 9183 . . . . . . . . 9 ;
283244, 245, 247, 282lesubd 9586 . . . . . . . 8 ;
28430recnd 9070 . . . . . . . . . 10
28555recnd 9070 . . . . . . . . . 10 ;
286284, 285, 61subdird 9446 . . . . . . . . 9 ; ;
28754recnd 9070 . . . . . . . . . . . 12 ;
288234, 287, 61mulassd 9067 . . . . . . . . . . 11 ; ;
28960, 61, 61mulassd 9067 . . . . . . . . . . . . 13 ; ;
29061sqvald 11475 . . . . . . . . . . . . . 14
291290oveq2d 6056 . . . . . . . . . . . . 13 ; ;
29251rpcnd 10606 . . . . . . . . . . . . . 14 ;
293240recnd 9070 . . . . . . . . . . . . . 14
294118, 292, 293mulassd 9067 . . . . . . . . . . . . 13 ; ;
295289, 291, 2943eqtr2d 2442 . . . . . . . . . . . 12 ; ;
296295oveq2d 6056 . . . . . . . . . . 11 ; ;
297288, 296eqtrd 2436 . . . . . . . . . 10 ; ;
298297oveq2d 6056 . . . . . . . . 9 ; ;
299286, 298eqtrd 2436 . . . . . . . 8 ; ;
300283, 299breqtrrd 4198 . . . . . . 7 ;
301247, 56, 132ledivmul2d 10654 . . . . . . 7 ; ;
302300, 301mpbird 224 . . . . . 6 ;
303239, 302eqbrtrrd 4194 . . . . 5 ;
304148, 56, 57, 303leadd1dd 9596 . . . 4 ;
30525, 149, 58, 232, 304letrd 9183 . . 3 ;
306 remulcl 9031 . . . . . . . . 9
30726, 27, 306sylancl 644 . . . . . . . 8
308307, 57readdcld 9071 . . . . . . 7
30916simp3d 971 . . . . . . . 8 ;
310309simp3d 971 . . . . . . 7 ;
311308, 54, 126, 310leadd2dd 9597 . . . . . 6 ;
31228recnd 9070 . . . . . . . . 9
31359, 61, 312adddid 9068 . . . . . . . 8
314313oveq1d 6055 . . . . . . 7
315126recnd 9070 . . . . . . . 8
31659, 312mulcld 9064 . . . . . . . 8
31713rpcnd 10606 . . . . . . . 8
318315, 316, 317addassd 9066 . . . . . . 7
319314, 318eqtrd 2436 . . . . . 6
3202872timesd 10166 . . . . . . . 8 ; ; ;
321320oveq2d 6056 . . . . . . 7 ; ; ; ; ;
322315, 287, 287nppcan3d 9394 . . . . . . 7 ; ; ; ;
323321, 322eqtrd 2436 . . . . . 6 ; ; ;
324311, 319, 3233brtr4d 4202 . . . . 5 ;