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

Theorem rlimcnp2 23052
 Description: Relate a limit of a real-valued sequence at infinity to the continuity of the function at zero. (Contributed by Mario Carneiro, 1-Mar-2015.)
Hypotheses
Ref Expression
rlimcnp2.a
rlimcnp2.0
rlimcnp2.b
rlimcnp2.c
rlimcnp2.r
rlimcnp2.d
rlimcnp2.s
rlimcnp2.j fld
rlimcnp2.k t
Assertion
Ref Expression
rlimcnp2
Distinct variable groups:   ,,   ,,   ,,   ,,   ,   ,
Allowed substitution hints:   ()   ()   (,)   (,)

Proof of Theorem rlimcnp2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 3718 . . . . . . . 8
2 resmpt 5323 . . . . . . . 8
31, 2mp1i 12 . . . . . . 7
4 0xr 9640 . . . . . . . . . . 11
5 0lt1 10075 . . . . . . . . . . 11
6 df-ioo 11533 . . . . . . . . . . . 12
7 df-ico 11535 . . . . . . . . . . . 12
8 xrltletr 11360 . . . . . . . . . . . 12
96, 7, 8ixxss1 11547 . . . . . . . . . . 11
104, 5, 9mp2an 672 . . . . . . . . . 10
11 ioorp 11602 . . . . . . . . . 10
1210, 11sseqtri 3536 . . . . . . . . 9
13 sslin 3724 . . . . . . . . 9
1412, 13ax-mp 5 . . . . . . . 8
15 resmpt 5323 . . . . . . . 8
1614, 15mp1i 12 . . . . . . 7
173, 16eqtr4d 2511 . . . . . 6
18 resres 5286 . . . . . 6
19 resres 5286 . . . . . 6
2017, 18, 193eqtr4g 2533 . . . . 5
21 rlimcnp2.r . . . . . . . . 9
22 eqid 2467 . . . . . . . . 9
2321, 22fmptd 6045 . . . . . . . 8
24 ffn 5731 . . . . . . . 8
2523, 24syl 16 . . . . . . 7
26 fnresdm 5690 . . . . . . 7
2725, 26syl 16 . . . . . 6
2827reseq1d 5272 . . . . 5
29 inss1 3718 . . . . . . . . . . 11
3029sseli 3500 . . . . . . . . . 10
3130, 21sylan2 474 . . . . . . . . 9
32 eqid 2467 . . . . . . . . 9
3331, 32fmptd 6045 . . . . . . . 8
34 frel 5734 . . . . . . . 8
3533, 34syl 16 . . . . . . 7
36 fdm 5735 . . . . . . . . 9
3733, 36syl 16 . . . . . . . 8
3837, 29syl6eqss 3554 . . . . . . 7
39 relssres 5311 . . . . . . 7
4035, 38, 39syl2anc 661 . . . . . 6
4140reseq1d 5272 . . . . 5
4220, 28, 413eqtr3d 2516 . . . 4
4342breq1d 4457 . . 3
44 rlimcnp2.b . . . 4
45 1red 9611 . . . 4
4623, 44, 45rlimresb 13351 . . 3
4729, 44syl5ss 3515 . . . 4
4833, 47, 45rlimresb 13351 . . 3
4943, 46, 483bitr4d 285 . 2
50 inss2 3719 . . . . . . . . . . 11
5150a1i 11 . . . . . . . . . 10
5251sselda 3504 . . . . . . . . 9
5352rpreccld 11266 . . . . . . . 8
5453rpne0d 11261 . . . . . . 7
5554neneqd 2669 . . . . . 6
56 iffalse 3948 . . . . . 6
5755, 56syl 16 . . . . 5
58 oveq2 6292 . . . . . . . . . 10
59 rpcnne0 11237 . . . . . . . . . . 11
60 recrec 10241 . . . . . . . . . . 11
6152, 59, 603syl 20 . . . . . . . . . 10
6258, 61sylan9eqr 2530 . . . . . . . . 9
6362eqcomd 2475 . . . . . . . 8
64 rlimcnp2.s . . . . . . . 8
6563, 64syl 16 . . . . . . 7
6665eqcomd 2475 . . . . . 6
6753, 66csbied 3462 . . . . 5
6857, 67eqtrd 2508 . . . 4
6968mpteq2dva 4533 . . 3
7069breq1d 4457 . 2
71 rlimcnp2.a . . . 4
72 rlimcnp2.0 . . . 4
73 rlimcnp2.c . . . . . 6
7473ad2antrr 725 . . . . 5
7571sselda 3504 . . . . . . . . . . . 12
76 0re 9596 . . . . . . . . . . . . 13
77 pnfxr 11321 . . . . . . . . . . . . 13
78 elico2 11588 . . . . . . . . . . . . 13
7976, 77, 78mp2an 672 . . . . . . . . . . . 12
8075, 79sylib 196 . . . . . . . . . . 11
8180simp1d 1008 . . . . . . . . . 10
8281adantr 465 . . . . . . . . 9
8380simp2d 1009 . . . . . . . . . . . . . 14
84 leloe 9671 . . . . . . . . . . . . . . 15
8576, 81, 84sylancr 663 . . . . . . . . . . . . . 14
8683, 85mpbid 210 . . . . . . . . . . . . 13
8786ord 377 . . . . . . . . . . . 12
88 eqcom 2476 . . . . . . . . . . . 12
8987, 88syl6ib 226 . . . . . . . . . . 11
9089con1d 124 . . . . . . . . . 10
9190imp 429 . . . . . . . . 9
9282, 91elrpd 11254 . . . . . . . 8
93 rpcnne0 11237 . . . . . . . . 9
94 recrec 10241 . . . . . . . . 9
9593, 94syl 16 . . . . . . . 8
9692, 95syl 16 . . . . . . 7
9796csbeq1d 3442 . . . . . 6
98 simplr 754 . . . . . . . . 9
99 simpll 753 . . . . . . . . . 10
100 rpreccl 11243 . . . . . . . . . . . . 13
101100adantl 466 . . . . . . . . . . . 12
102 rlimcnp2.d . . . . . . . . . . . . . 14
103102ralrimiva 2878 . . . . . . . . . . . . 13
104103adantr 465 . . . . . . . . . . . 12
105 eleq1 2539 . . . . . . . . . . . . . 14
106 oveq2 6292 . . . . . . . . . . . . . . 15
107106eleq1d 2536 . . . . . . . . . . . . . 14
108105, 107bibi12d 321 . . . . . . . . . . . . 13
109108rspcv 3210 . . . . . . . . . . . 12
110101, 104, 109sylc 60 . . . . . . . . . . 11
11195adantl 466 . . . . . . . . . . . 12
112111eleq1d 2536 . . . . . . . . . . 11
113110, 112bitr2d 254 . . . . . . . . . 10
11499, 92, 113syl2anc 661 . . . . . . . . 9
11598, 114mpbid 210 . . . . . . . 8
11692rpreccld 11266 . . . . . . . 8
117115, 116elind 3688 . . . . . . 7
11867, 31eqeltrd 2555 . . . . . . . . 9
119118ralrimiva 2878 . . . . . . . 8
120119ad2antrr 725 . . . . . . 7
121106csbeq1d 3442 . . . . . . . . 9
122121eleq1d 2536 . . . . . . . 8
123122rspcv 3210 . . . . . . 7
124117, 120, 123sylc 60 . . . . . 6
12597, 124eqeltrrd 2556 . . . . 5
12674, 125ifclda 3971 . . . 4
127101biantrud 507 . . . . . 6
128113, 127bitrd 253 . . . . 5
129 elin 3687 . . . . 5
130128, 129syl6bbr 263 . . . 4
131 iftrue 3945 . . . 4
132 eqeq1 2471 . . . . 5
133 csbeq1 3438 . . . . 5
134132, 133ifbieq2d 3964 . . . 4
135 rlimcnp2.j . . . 4 fld
136 rlimcnp2.k . . . 4 t
13771, 72, 51, 126, 130, 131, 134, 135, 136rlimcnp 23051 . . 3
138 nfcv 2629 . . . . 5
139 nfv 1683 . . . . . 6
140 nfcv 2629 . . . . . 6
141 nfcsb1v 3451 . . . . . 6
142139, 140, 141nfif 3968 . . . . 5
143 eqeq1 2471 . . . . . 6
144 csbeq1a 3444 . . . . . 6
145143, 144ifbieq2d 3964 . . . . 5
146138, 142, 145cbvmpt 4537 . . . 4
147146eleq1i 2544 . . 3
148137, 147syl6bbr 263 . 2
14949, 70, 1483bitr2d 281 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wo 368   wa 369   w3a 973   wceq 1379   wcel 1767   wne 2662  wral 2814  csb 3435   cin 3475   wss 3476  cif 3939   class class class wbr 4447   cmpt 4505   cdm 4999   cres 5001   wrel 5004   wfn 5583  wf 5584  cfv 5588  (class class class)co 6284  cc 9490  cr 9491  cc0 9492  c1 9493   cpnf 9625  cxr 9627   clt 9628   cle 9629   cdiv 10206  crp 11220  cioo 11529  cico 11531   crli 13271   ↾t crest 14676  ctopn 14677  ℂfldccnfld 18219   ccnp 19520 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569  ax-pre-sup 9570 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-1st 6784  df-2nd 6785  df-recs 7042  df-rdg 7076  df-1o 7130  df-oadd 7134  df-er 7311  df-map 7422  df-pm 7423  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-sup 7901  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-div 10207  df-nn 10537  df-2 10594  df-3 10595  df-4 10596  df-5 10597  df-6 10598  df-7 10599  df-8 10600  df-9 10601  df-10 10602  df-n0 10796  df-z 10865  df-dec 10977  df-uz 11083  df-q 11183  df-rp 11221  df-xneg 11318  df-xadd 11319  df-xmul 11320  df-ioo 11533  df-ico 11535  df-fz 11673  df-seq 12076  df-exp 12135  df-cj 12895  df-re 12896  df-im 12897  df-sqrt 13031  df-abs 13032  df-rlim 13275  df-struct 14492  df-ndx 14493  df-slot 14494  df-base 14495  df-plusg 14568  df-mulr 14569  df-starv 14570  df-tset 14574  df-ple 14575  df-ds 14577  df-unif 14578  df-rest 14678  df-topn 14679  df-topgen 14699  df-psmet 18210  df-xmet 18211  df-met 18212  df-bl 18213  df-mopn 18214  df-cnfld 18220  df-top 19194  df-bases 19196  df-topon 19197  df-cnp 19523 This theorem is referenced by:  rlimcnp3  23053
 Copyright terms: Public domain W3C validator