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

Theorem pntlemb 21274
 Description: Lemma for pnt 21291. Unpack all the lower bounds contained in , in the form they will be used. For comparison with Equation 10.6.27 of [Shapiro], p. 434, is x. (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
Assertion
Ref Expression
pntlemb ;
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem pntlemb
StepHypRef Expression
1 pntlem1.z . . . . 5
2 pntlem1.r . . . . . . . 8 ψ
3 pntlem1.a . . . . . . . 8
4 pntlem1.b . . . . . . . 8
5 pntlem1.l . . . . . . . 8
6 pntlem1.d . . . . . . . 8
7 pntlem1.f . . . . . . . 8 ;
8 pntlem1.u . . . . . . . 8
9 pntlem1.u2 . . . . . . . 8
10 pntlem1.e . . . . . . . 8
11 pntlem1.k . . . . . . . 8
12 pntlem1.y . . . . . . . 8
13 pntlem1.x . . . . . . . 8
14 pntlem1.c . . . . . . . 8
15 pntlem1.w . . . . . . . 8 ;
162, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15pntlema 21273 . . . . . . 7
1716rpred 10632 . . . . . 6
18 pnfxr 10697 . . . . . 6
19 elico2 10958 . . . . . 6
2017, 18, 19sylancl 644 . . . . 5
211, 20mpbid 202 . . . 4
2221simp1d 969 . . 3
2321simp2d 970 . . 3
2422, 16, 23rpgecld 10667 . 2
25 1re 9074 . . . . . . 7
2625a1i 11 . . . . . 6
27 ere 12674 . . . . . . 7
2827a1i 11 . . . . . 6
2924rpsqrcld 12197 . . . . . . 7
3029rpred 10632 . . . . . 6
31 1lt2 10126 . . . . . . . 8
32 egt2lt3 12788 . . . . . . . . 9
3332simpli 445 . . . . . . . 8
34 2re 10053 . . . . . . . . 9
3525, 34, 27lttri 9183 . . . . . . . 8
3631, 33, 35mp2an 654 . . . . . . 7
3736a1i 11 . . . . . 6
38 4re 10057 . . . . . . . 8
3938a1i 11 . . . . . . 7
4032simpri 449 . . . . . . . . 9
41 3lt4 10129 . . . . . . . . 9
42 3re 10055 . . . . . . . . . 10
4327, 42, 38lttri 9183 . . . . . . . . 9
4440, 41, 43mp2an 654 . . . . . . . 8
4544a1i 11 . . . . . . 7
46 4nn 10119 . . . . . . . . . . 11
47 nnrp 10605 . . . . . . . . . . 11
4846, 47ax-mp 8 . . . . . . . . . 10
492, 3, 4, 5, 6, 7pntlemd 21271 . . . . . . . . . . . 12
5049simp1d 969 . . . . . . . . . . 11
512, 3, 4, 5, 6, 7, 8, 9, 10, 11pntlemc 21272 . . . . . . . . . . . 12
5251simp1d 969 . . . . . . . . . . 11
5350, 52rpmulcld 10648 . . . . . . . . . 10
54 rpdivcl 10618 . . . . . . . . . 10
5548, 53, 54sylancr 645 . . . . . . . . 9
5655rpred 10632 . . . . . . . 8
5753rpred 10632 . . . . . . . . . . . 12
5852rpred 10632 . . . . . . . . . . . 12
5950rpred 10632 . . . . . . . . . . . . . 14
60 eliooord 10954 . . . . . . . . . . . . . . . 16
615, 60syl 16 . . . . . . . . . . . . . . 15
6261simprd 450 . . . . . . . . . . . . . 14
6359, 26, 52, 62ltmul1dd 10683 . . . . . . . . . . . . 13
6452rpcnd 10634 . . . . . . . . . . . . . 14
6564mulid2d 9090 . . . . . . . . . . . . 13
6663, 65breqtrd 4223 . . . . . . . . . . . 12
6751simp3d 971 . . . . . . . . . . . . . . 15
6867simp1d 969 . . . . . . . . . . . . . 14
69 eliooord 10954 . . . . . . . . . . . . . 14
7068, 69syl 16 . . . . . . . . . . . . 13
7170simprd 450 . . . . . . . . . . . 12
7257, 58, 26, 66, 71lttrd 9215 . . . . . . . . . . 11
73 4pos 10070 . . . . . . . . . . . . 13
7439, 73jctir 525 . . . . . . . . . . . 12
75 ltmul2 9845 . . . . . . . . . . . 12
7657, 26, 74, 75syl3anc 1184 . . . . . . . . . . 11
7772, 76mpbid 202 . . . . . . . . . 10
78 4cn 10058 . . . . . . . . . . 11
7978mulid1i 9076 . . . . . . . . . 10
8077, 79syl6breq 4238 . . . . . . . . 9
8139, 39, 53ltmuldivd 10675 . . . . . . . . 9
8280, 81mpbid 202 . . . . . . . 8
8312simpld 446 . . . . . . . . . . 11
8483, 55rpaddcld 10647 . . . . . . . . . 10
8584rpred 10632 . . . . . . . . 9
8656, 83ltaddrp2d 10662 . . . . . . . . 9
8785resqcld 11532 . . . . . . . . . . . 12
8813simpld 446 . . . . . . . . . . . . . . . . 17
8951simp2d 970 . . . . . . . . . . . . . . . . . 18
90 2z 10296 . . . . . . . . . . . . . . . . . 18
91 rpexpcl 11383 . . . . . . . . . . . . . . . . . 18
9289, 90, 91sylancl 644 . . . . . . . . . . . . . . . . 17
9388, 92rpmulcld 10648 . . . . . . . . . . . . . . . 16
9446nnzi 10289 . . . . . . . . . . . . . . . 16
95 rpexpcl 11383 . . . . . . . . . . . . . . . 16
9693, 94, 95sylancl 644 . . . . . . . . . . . . . . 15
97 3nn0 10223 . . . . . . . . . . . . . . . . . . . . . 22
98 2nn 10117 . . . . . . . . . . . . . . . . . . . . . 22
9997, 98decnncl 10379 . . . . . . . . . . . . . . . . . . . . 21 ;
100 nnrp 10605 . . . . . . . . . . . . . . . . . . . . 21 ; ;
10199, 100ax-mp 8 . . . . . . . . . . . . . . . . . . . 20 ;
102 rpmulcl 10617 . . . . . . . . . . . . . . . . . . . 20 ; ;
103101, 4, 102sylancr 645 . . . . . . . . . . . . . . . . . . 19 ;
10467simp3d 971 . . . . . . . . . . . . . . . . . . . 20
105 rpexpcl 11383 . . . . . . . . . . . . . . . . . . . . . 22
10652, 90, 105sylancl 644 . . . . . . . . . . . . . . . . . . . . 21
10750, 106rpmulcld 10648 . . . . . . . . . . . . . . . . . . . 20
108104, 107rpmulcld 10648 . . . . . . . . . . . . . . . . . . 19
109103, 108rpdivcld 10649 . . . . . . . . . . . . . . . . . 18 ;
110 3nn 10118 . . . . . . . . . . . . . . . . . . . . 21
111 nnrp 10605 . . . . . . . . . . . . . . . . . . . . 21
112110, 111ax-mp 8 . . . . . . . . . . . . . . . . . . . 20
113 rpmulcl 10617 . . . . . . . . . . . . . . . . . . . 20
1148, 112, 113sylancl 644 . . . . . . . . . . . . . . . . . . 19
115114, 14rpaddcld 10647 . . . . . . . . . . . . . . . . . 18
116109, 115rpmulcld 10648 . . . . . . . . . . . . . . . . 17 ;
117116rpred 10632 . . . . . . . . . . . . . . . 16 ;
118117rpefcld 12689 . . . . . . . . . . . . . . 15 ;
11996, 118rpaddcld 10647 . . . . . . . . . . . . . 14 ;
12087, 119ltaddrpd 10661 . . . . . . . . . . . . 13 ;
121120, 15syl6breqr 4239 . . . . . . . . . . . 12
12287, 17, 22, 121, 23ltletrd 9214 . . . . . . . . . . 11
12324rprege0d 10639 . . . . . . . . . . . 12
124 resqrth 12044 . . . . . . . . . . . 12
125123, 124syl 16 . . . . . . . . . . 11
126122, 125breqtrrd 4225 . . . . . . . . . 10
12784rprege0d 10639 . . . . . . . . . . 11
12829rprege0d 10639 . . . . . . . . . . 11
129 lt2sq 11438 . . . . . . . . . . 11
130127, 128, 129syl2anc 643 . . . . . . . . . 10
131126, 130mpbird 224 . . . . . . . . 9
13256, 85, 30, 86, 131lttrd 9215 . . . . . . . 8
13339, 56, 30, 82, 132lttrd 9215 . . . . . . 7
13428, 39, 30, 45, 133lttrd 9215 . . . . . 6
13526, 28, 30, 37, 134lttrd 9215 . . . . 5
136 0le1 9535 . . . . . . 7
137136a1i 11 . . . . . 6
138 lt2sq 11438 . . . . . 6
13926, 137, 128, 138syl21anc 1183 . . . . 5
140135, 139mpbid 202 . . . 4
141 sq1 11459 . . . . 5
142141a1i 11 . . . 4
143140, 142, 1253brtr3d 4228 . . 3
14428, 30, 134ltled 9205 . . 3
14522, 83rerpdivcld 10659 . . . 4
14683rpred 10632 . . . . . . 7
147146, 55ltaddrpd 10661 . . . . . . . 8
148146, 85, 30, 147, 131lttrd 9215 . . . . . . 7
149146, 30, 29, 148ltmul2dd 10684 . . . . . 6
150 remsqsqr 12045 . . . . . . 7
151123, 150syl 16 . . . . . 6
152149, 151breqtrd 4223 . . . . 5
15330, 22, 83ltmuldivd 10675 . . . . 5
154152, 153mpbid 202 . . . 4
15530, 145, 154ltled 9205 . . 3
156143, 144, 1553jca 1134 . 2
15756, 30, 132ltled 9205 . . 3
15888relogcld 20501 . . . . . 6
15989rpred 10632 . . . . . . 7
16067simp2d 970 . . . . . . 7
161159, 160rplogcld 20507 . . . . . 6
162158, 161rerpdivcld 10659 . . . . 5
163 readdcl 9057 . . . . 5
164162, 34, 163sylancl 644 . . . 4
16524relogcld 20501 . . . . . 6
166165, 161rerpdivcld 10659 . . . . 5
167 nndivre 10019 . . . . 5
168166, 46, 167sylancl 644 . . . 4
16993relogcld 20501 . . . . . 6
170 nndivre 10019 . . . . . . 7
171165, 46, 170sylancl 644 . . . . . 6
172 relogexp 20473 . . . . . . . . 9
17393, 94, 172sylancl 644 . . . . . . . 8
17496rpred 10632 . . . . . . . . . 10
175119rpred 10632 . . . . . . . . . 10 ;
176174, 118ltaddrpd 10661 . . . . . . . . . 10 ;
177 rpexpcl 11383 . . . . . . . . . . . . . 14
17884, 90, 177sylancl 644 . . . . . . . . . . . . 13
179175, 178ltaddrpd 10661 . . . . . . . . . . . 12 ; ;
18087recnd 9098 . . . . . . . . . . . . . 14
181119rpcnd 10634 . . . . . . . . . . . . . 14 ;
182180, 181addcomd 9252 . . . . . . . . . . . . 13 ; ;
18315, 182syl5eq 2474 . . . . . . . . . . . 12 ;
184179, 183breqtrrd 4225 . . . . . . . . . . 11 ;
185175, 17, 22, 184, 23ltletrd 9214 . . . . . . . . . 10 ;
186174, 175, 22, 176, 185lttrd 9215 . . . . . . . . 9
187 logltb 20477 . . . . . . . . . 10
18896, 24, 187syl2anc 643 . . . . . . . . 9
189186, 188mpbid 202 . . . . . . . 8
190173, 189eqbrtrrd 4221 . . . . . . 7
191 ltmuldiv2 9865 . . . . . . . 8
192169, 165, 74, 191syl3anc 1184 . . . . . . 7
193190, 192mpbid 202 . . . . . 6
194169, 171, 161, 193ltdiv1dd 10685 . . . . 5
19588, 92relogmuld 20503 . . . . . . . 8
196 relogexp 20473 . . . . . . . . . 10
19789, 90, 196sylancl 644 . . . . . . . . 9
198197oveq2d 6083 . . . . . . . 8
199195, 198eqtrd 2462 . . . . . . 7
200199oveq1d 6082 . . . . . 6
201158recnd 9098 . . . . . . 7
20234a1i 11 . . . . . . . . 9
203202recnd 9098 . . . . . . . 8
204161rpcnd 10634 . . . . . . . 8
205203, 204mulcld 9092 . . . . . . 7
206161rpcnne0d 10641 . . . . . . 7
207 divdir 9685 . . . . . . 7
208201, 205, 206, 207syl3anc 1184 . . . . . 6
209206simprd 450 . . . . . . . 8
210203, 204, 209divcan4d 9780 . . . . . . 7
211210oveq2d 6083 . . . . . 6
212200, 208, 2113eqtrd 2466 . . . . 5
213165recnd 9098 . . . . . 6
214 rpcnne0 10613 . . . . . . 7
21548, 214mp1i 12 . . . . . 6
216 divdiv32 9706 . . . . . 6
217213, 215, 206, 216syl3anc 1184 . . . . 5
218194, 212, 2173brtr3d 4228 . . . 4
219164, 168, 218ltled 9205 . . 3
220115rpred 10632 . . . . 5
221108, 103rpdivcld 10649 . . . . . . 7 ;
222221rpred 10632 . . . . . 6 ;
223222, 165remulcld 9100 . . . . 5 ;
224115rpcnd 10634 . . . . . . . . 9
225108rpcnne0d 10641 . . . . . . . . 9
226103rpcnne0d 10641 . . . . . . . . 9 ; ;
227 divdiv2 9710 . . . . . . . . 9 ; ; ; ;
228224, 225, 226, 227syl3anc 1184 . . . . . . . 8 ; ;
229103rpcnd 10634 . . . . . . . . . 10 ;
230224, 229mulcomd 9093 . . . . . . . . 9 ; ;
231230oveq1d 6082 . . . . . . . 8 ; ;
232 div23 9681 . . . . . . . . 9 ; ; ;
233229, 224, 225, 232syl3anc 1184 . . . . . . . 8 ; ;
234228, 231, 2333eqtrd 2466 . . . . . . 7 ; ;
235117reefcld 12673 . . . . . . . . . 10 ;
236235, 96ltaddrp2d 10662 . . . . . . . . . 10 ; ;
237235, 175, 22, 236, 185lttrd 9215 . . . . . . . . 9 ;
23824reeflogd 20502 . . . . . . . . 9
239237, 238breqtrrd 4225 . . . . . . . 8 ;
240 eflt 12701 . . . . . . . . 9 ; ; ;
241117, 165, 240syl2anc 643 . . . . . . . 8 ; ;
242239, 241mpbird 224 . . . . . . 7 ;
243234, 242eqbrtrd 4219 . . . . . 6 ;
244220, 165, 221ltdivmuld 10679 . . . . . 6 ; ;
245243, 244mpbid 202 . . . . 5 ;
246220, 223, 245ltled 9205 . . . 4 ;
247104rpcnd 10634 . . . . . 6
248107rpcnd 10634 . . . . . 6
249 divass 9680 . . . . . 6 ; ; ; ;
250247, 248, 226, 249syl3anc 1184 . . . . 5 ; ;
251250oveq1d 6082 . . . 4 ; ;
252246, 251breqtrd 4223 . . 3 ;
253157, 219, 2523jca 1134 . 2 ;
25424, 156, 2533jca 1134 1 ;
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936   wceq 1652   wcel 1725   wne 2593   class class class wbr 4199   cmpt 4253  cfv 5440  (class class class)co 6067  cc 8972  cr 8973  cc0 8974  c1 8975   caddc 8977   cmul 8979   cpnf 9101  cxr 9103   clt 9104   cle 9105   cmin 9275   cdiv 9661  cn 9984  c2 10033  c3 10034  c4 10035  cz 10266  ;cdc 10366  crp 10596  cioo 10900  cico 10902  cexp 11365  csqr 12021  ce 12647  ceu 12648  clog 20435  ψcchp 20858 This theorem is referenced by:  pntlemg  21275  pntlemh  21276  pntlemn  21277  pntlemq  21278  pntlemr  21279  pntlemj  21280  pntlemf  21282  pntlemk  21283  pntlemo  21284 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-rep 4307  ax-sep 4317  ax-nul 4325  ax-pow 4364  ax-pr 4390  ax-un 4687  ax-inf2 7580  ax-cnex 9030  ax-resscn 9031  ax-1cn 9032  ax-icn 9033  ax-addcl 9034  ax-addrcl 9035  ax-mulcl 9036  ax-mulrcl 9037  ax-mulcom 9038  ax-addass 9039  ax-mulass 9040  ax-distr 9041  ax-i2m1 9042  ax-1ne0 9043  ax-1rid 9044  ax-rnegex 9045  ax-rrecex 9046  ax-cnre 9047  ax-pre-lttri 9048  ax-pre-lttrn 9049  ax-pre-ltadd 9050  ax-pre-mulgt0 9051  ax-pre-sup 9052  ax-addf 9053  ax-mulf 9054 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-nel 2596  df-ral 2697  df-rex 2698  df-reu 2699  df-rmo 2700  df-rab 2701  df-v 2945  df-sbc 3149  df-csb 3239  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-pss 3323  df-nul 3616  df-if 3727  df-pw 3788  df-sn 3807  df-pr 3808  df-tp 3809  df-op 3810  df-uni 4003  df-int 4038  df-iun 4082  df-iin 4083  df-br 4200  df-opab 4254  df-mpt 4255  df-tr 4290  df-eprel 4481  df-id 4485  df-po 4490  df-so 4491  df-fr 4528  df-se 4529  df-we 4530  df-ord 4571  df-on 4572  df-lim 4573  df-suc 4574  df-om 4832  df-xp 4870  df-rel 4871  df-cnv 4872  df-co 4873  df-dm 4874  df-rn 4875  df-res 4876  df-ima 4877  df-iota 5404  df-fun 5442  df-fn 5443  df-f 5444  df-f1 5445  df-fo 5446  df-f1o 5447  df-fv 5448  df-isom 5449  df-ov 6070  df-oprab 6071  df-mpt2 6072  df-of 6291  df-1st 6335  df-2nd 6336  df-riota 6535  df-recs 6619  df-rdg 6654  df-1o 6710  df-2o 6711  df-oadd 6714  df-er 6891  df-map 7006  df-pm 7007  df-ixp 7050  df-en 7096  df-dom 7097  df-sdom 7098  df-fin 7099  df-fi 7402  df-sup 7432  df-oi 7463  df-card 7810  df-cda 8032  df-pnf 9106  df-mnf 9107  df-xr 9108  df-ltxr 9109  df-le 9110  df-sub 9277  df-neg 9278  df-div 9662  df-nn 9985  df-2 10042  df-3 10043  df-4 10044  df-5 10045  df-6 10046  df-7 10047  df-8 10048  df-9 10049  df-10 10050  df-n0 10206  df-z 10267  df-dec 10367  df-uz 10473  df-q 10559  df-rp 10597  df-xneg 10694  df-xadd 10695  df-xmul 10696  df-ioo 10904  df-ioc 10905  df-ico 10906  df-icc 10907  df-fz 11028  df-fzo 11119  df-fl 11185  df-mod 11234  df-seq 11307  df-exp 11366  df-fac 11550  df-bc 11577  df-hash 11602  df-shft 11865  df-cj 11887  df-re 11888  df-im 11889  df-sqr 12023  df-abs 12024  df-limsup 12248  df-clim 12265  df-rlim 12266  df-sum 12463  df-ef 12653  df-e 12654  df-sin 12655  df-cos 12656  df-pi 12658  df-struct 13454  df-ndx 13455  df-slot 13456  df-base 13457  df-sets 13458  df-ress 13459  df-plusg 13525  df-mulr 13526  df-starv 13527  df-sca 13528  df-vsca 13529  df-tset 13531  df-ple 13532  df-ds 13534  df-unif 13535  df-hom 13536  df-cco 13537  df-rest 13633  df-topn 13634  df-topgen 13650  df-pt 13651  df-prds 13654  df-xrs 13709  df-0g 13710  df-gsum 13711  df-qtop 13716  df-imas 13717  df-xps 13719  df-mre 13794  df-mrc 13795  df-acs 13797  df-mnd 14673  df-submnd 14722  df-mulg 14798  df-cntz 15099  df-cmn 15397  df-psmet 16677  df-xmet 16678  df-met 16679  df-bl 16680  df-mopn 16681  df-fbas 16682  df-fg 16683  df-cnfld 16687  df-top 16946  df-bases 16948  df-topon 16949  df-topsp 16950  df-cld 17066  df-ntr 17067  df-cls 17068  df-nei 17145  df-lp 17183  df-perf 17184  df-cn 17274  df-cnp 17275  df-haus 17362  df-tx 17577  df-hmeo 17770  df-fil 17861  df-fm 17953  df-flim 17954  df-flf 17955  df-xms 18333  df-ms 18334  df-tms 18335  df-cncf 18891  df-limc 19736  df-dv 19737  df-log 20437
 Copyright terms: Public domain W3C validator