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

Theorem xrlimcnp 20485
 Description: Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at . Since any limit can be written in the form on the left side of the implication, this shows that real limits are a special case of topological continuity at a point. (Contributed by Mario Carneiro, 8-Sep-2015.)
Hypotheses
Ref Expression
xrlimcnp.a
xrlimcnp.b
xrlimcnp.r
xrlimcnp.c
xrlimcnp.j fld
xrlimcnp.k ordTop t
Assertion
Ref Expression
xrlimcnp
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem xrlimcnp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrlimcnp.r . . . . 5
2 eqid 2366 . . . . 5
31, 2fmptd 5795 . . . 4
5 ssun2 3427 . . . . . . . . . 10
6 pnfxr 10606 . . . . . . . . . . . 12
76elexi 2882 . . . . . . . . . . 11
87snid 3756 . . . . . . . . . 10
95, 8sselii 3263 . . . . . . . . 9
10 xrlimcnp.a . . . . . . . . 9
119, 10syl5eleqr 2453 . . . . . . . 8
121ralrimiva 2711 . . . . . . . . 9
13 xrlimcnp.c . . . . . . . . . . 11
1413eleq1d 2432 . . . . . . . . . 10
1514rspcv 2965 . . . . . . . . 9
1611, 12, 15sylc 56 . . . . . . . 8
1713, 2fvmptg 5707 . . . . . . . 8
1811, 16, 17syl2anc 642 . . . . . . 7
1918ad2antrr 706 . . . . . 6
2019eleq1d 2432 . . . . 5
21 cnxmet 18495 . . . . . . . 8
22 xrlimcnp.j . . . . . . . . . 10 fld
2322cnfldtopn 18504 . . . . . . . . 9
2423mopni2 18252 . . . . . . . 8
2521, 24mp3an1 1265 . . . . . . 7
26 ssun1 3426 . . . . . . . . . . . . . 14
2726, 10syl5sseqr 3313 . . . . . . . . . . . . 13
28 ssralv 3323 . . . . . . . . . . . . 13
2927, 12, 28sylc 56 . . . . . . . . . . . 12
3029ad2antrr 706 . . . . . . . . . . 11
31 simprl 732 . . . . . . . . . . 11
32 simplr 731 . . . . . . . . . . 11
3330, 31, 32rlimi 12194 . . . . . . . . . 10
34 letop 17153 . . . . . . . . . . . . . . . . 17 ordTop
3534a1i 10 . . . . . . . . . . . . . . . 16 ordTop
36 xrlimcnp.b . . . . . . . . . . . . . . . . . . . . 21
37 ressxr 9023 . . . . . . . . . . . . . . . . . . . . 21
3836, 37syl6ss 3277 . . . . . . . . . . . . . . . . . . . 20
396a1i 10 . . . . . . . . . . . . . . . . . . . . 21
4039snssd 3858 . . . . . . . . . . . . . . . . . . . 20
4138, 40unssd 3439 . . . . . . . . . . . . . . . . . . 19
4210, 41eqsstrd 3298 . . . . . . . . . . . . . . . . . 18
43 xrex 10502 . . . . . . . . . . . . . . . . . . 19
4443ssex 4260 . . . . . . . . . . . . . . . . . 18
4542, 44syl 15 . . . . . . . . . . . . . . . . 17
4645ad2antrr 706 . . . . . . . . . . . . . . . 16
47 iocpnfordt 17162 . . . . . . . . . . . . . . . . 17 ordTop
4847a1i 10 . . . . . . . . . . . . . . . 16 ordTop
49 elrestr 13543 . . . . . . . . . . . . . . . 16 ordTop ordTop ordTop t
5035, 46, 48, 49syl3anc 1183 . . . . . . . . . . . . . . 15 ordTop t
51 xrlimcnp.k . . . . . . . . . . . . . . 15 ordTop t
5250, 51syl6eleqr 2457 . . . . . . . . . . . . . 14
53 simprl 732 . . . . . . . . . . . . . . . . 17
5453rexrd 9028 . . . . . . . . . . . . . . . 16
556a1i 10 . . . . . . . . . . . . . . . 16
56 ltpnf 10614 . . . . . . . . . . . . . . . . 17
5753, 56syl 15 . . . . . . . . . . . . . . . 16
58 ubioc1 10858 . . . . . . . . . . . . . . . 16
5954, 55, 57, 58syl3anc 1183 . . . . . . . . . . . . . . 15
6011ad2antrr 706 . . . . . . . . . . . . . . 15
61 elin 3446 . . . . . . . . . . . . . . 15
6259, 60, 61sylanbrc 645 . . . . . . . . . . . . . 14
63 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6463rexrd 9028 . . . . . . . . . . . . . . . . . . . . . . . . . 26
65 elioc1 10851 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6664, 6, 65sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . 25
67 simp2 957 . . . . . . . . . . . . . . . . . . . . . . . . 25
6866, 67syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . . 24
6936ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7069sselda 3266 . . . . . . . . . . . . . . . . . . . . . . . . 25
71 ltle 9057 . . . . . . . . . . . . . . . . . . . . . . . . 25
7263, 70, 71syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24
7368, 72syld 40 . . . . . . . . . . . . . . . . . . . . . . 23
7421a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . 26
75 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7675ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
77 rpxr 10512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7876, 77syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7916ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8029ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8180r19.21bi 2726 . . . . . . . . . . . . . . . . . . . . . . . . . 26
82 elbl3 18164 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8374, 78, 79, 81, 82syl22anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . 25
84 eqid 2366 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8584cnmetdval 18493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8681, 79, 85syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8786breq1d 4135 . . . . . . . . . . . . . . . . . . . . . . . . 25
8883, 87bitrd 244 . . . . . . . . . . . . . . . . . . . . . . . 24
8988biimprd 214 . . . . . . . . . . . . . . . . . . . . . . 23
9073, 89imim12d 68 . . . . . . . . . . . . . . . . . . . . . 22
9190ralimdva 2706 . . . . . . . . . . . . . . . . . . . . 21
9291impr 602 . . . . . . . . . . . . . . . . . . . 20
9321a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23
9416ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 23
95 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . 23
96 blcntr 18177 . . . . . . . . . . . . . . . . . . . . . . 23
9793, 94, 95, 96syl3anc 1183 . . . . . . . . . . . . . . . . . . . . . 22
9897a1d 22 . . . . . . . . . . . . . . . . . . . . 21
99 eleq1 2426 . . . . . . . . . . . . . . . . . . . . . . 23
10013eleq1d 2432 . . . . . . . . . . . . . . . . . . . . . . 23
10199, 100imbi12d 311 . . . . . . . . . . . . . . . . . . . . . 22
1027, 101ralsn 3764 . . . . . . . . . . . . . . . . . . . . 21
10398, 102sylibr 203 . . . . . . . . . . . . . . . . . . . 20
104 ralunb 3444 . . . . . . . . . . . . . . . . . . . 20
10592, 103, 104sylanbrc 645 . . . . . . . . . . . . . . . . . . 19
10610ad2antrr 706 . . . . . . . . . . . . . . . . . . . 20
107106raleqdv 2827 . . . . . . . . . . . . . . . . . . 19
108105, 107mpbird 223 . . . . . . . . . . . . . . . . . 18
109 ss2rab 3335 . . . . . . . . . . . . . . . . . 18
110108, 109sylibr 203 . . . . . . . . . . . . . . . . 17
111 incom 3449 . . . . . . . . . . . . . . . . . 18
112 dfin5 3246 . . . . . . . . . . . . . . . . . 18
113111, 112eqtri 2386 . . . . . . . . . . . . . . . . 17
1142mptpreima 5269 . . . . . . . . . . . . . . . . 17
115110, 113, 1143sstr4g 3305 . . . . . . . . . . . . . . . 16
116 funmpt 5393 . . . . . . . . . . . . . . . . 17
117 inss2 3478 . . . . . . . . . . . . . . . . . 18
1183ad2antrr 706 . . . . . . . . . . . . . . . . . . 19
119 fdm 5499 . . . . . . . . . . . . . . . . . . 19
120118, 119syl 15 . . . . . . . . . . . . . . . . . 18
121117, 120syl5sseqr 3313 . . . . . . . . . . . . . . . . 17
122 funimass3 5748 . . . . . . . . . . . . . . . . 17
123116, 121, 122sylancr 644 . . . . . . . . . . . . . . . 16
124115, 123mpbird 223 . . . . . . . . . . . . . . 15
125 simplrr 737 . . . . . . . . . . . . . . 15
126124, 125sstrd 3275 . . . . . . . . . . . . . 14
127 eleq2 2427 . . . . . . . . . . . . . . . 16
128 imaeq2 5111 . . . . . . . . . . . . . . . . 17
129128sseq1d 3291 . . . . . . . . . . . . . . . 16
130127, 129anbi12d 691 . . . . . . . . . . . . . . 15
131130rspcev 2969 . . . . . . . . . . . . . 14
13252, 62, 126, 131syl12anc 1181 . . . . . . . . . . . . 13
133132expr 598 . . . . . . . . . . . 12
134133rexlimdva 2752 . . . . . . . . . . 11
135134adantlr 695 . . . . . . . . . 10
13633, 135mpd 14 . . . . . . . . 9
137136expr 598 . . . . . . . 8
138137rexlimdva 2752 . . . . . . 7
13925, 138syl5 28 . . . . . 6
140139expdimp 426 . . . . 5
14120, 140sylbid 206 . . . 4
142141ralrimiva 2711 . . 3
143 letopon 17152 . . . . . . 7 ordTop TopOn
144 resttopon 17109 . . . . . . 7 ordTop TopOn ordTop t TopOn
145143, 42, 144sylancr 644 . . . . . 6 ordTop t TopOn
14651, 145syl5eqel 2450 . . . . 5 TopOn
14722cnfldtopon 18505 . . . . . 6 TopOn
148147a1i 10 . . . . 5 TopOn
149 iscnp 17184 . . . . 5 TopOn TopOn
150146, 148, 11, 149syl3anc 1183 . . . 4
1524, 142, 151mpbir2and 888 . 2
153 simplr 731 . . . . . . 7
15421a1i 10 . . . . . . . 8
15516ad2antrr 706 . . . . . . . 8
15677adantl 452 . . . . . . . 8
15723blopn 18259 . . . . . . . 8
158154, 155, 156, 157syl3anc 1183 . . . . . . 7
15918ad2antrr 706 . . . . . . . 8
160 simpr 447 . . . . . . . . 9
161154, 155, 160, 96syl3anc 1183 . . . . . . . 8
162159, 161eqeltrd 2440 . . . . . . 7
163 cnpimaex 17203 . . . . . . 7
164153, 158, 162, 163syl3anc 1183 . . . . . 6
165 vex 2876 . . . . . . . . 9
166165inex1 4257 . . . . . . . 8
167166a1i 10 . . . . . . 7 ordTop
16851eleq2i 2430 . . . . . . . 8 ordTop t
16945ad2antrr 706 . . . . . . . . 9
170 elrest 13542 . . . . . . . . 9 ordTop ordTop t ordTop
17134, 169, 170sylancr 644 . . . . . . . 8 ordTop t ordTop
172168, 171syl5bb 248 . . . . . . 7 ordTop
173 eleq2 2427 . . . . . . . . 9
174 imaeq2 5111 . . . . . . . . . 10
175174sseq1d 3291 . . . . . . . . 9
176173, 175anbi12d 691 . . . . . . . 8
177176adantl 452 . . . . . . 7
178167, 172, 177rexxfr2d 4654 . . . . . 6 ordTop
179164, 178mpbid 201 . . . . 5 ordTop
180 inss1 3477 . . . . . . . . . . . 12
181180sseli 3262 . . . . . . . . . . 11
182 pnfnei 17167 . . . . . . . . . . 11 ordTop
183181, 182sylan2 460 . . . . . . . . . 10 ordTop
184 df-ima 4805 . . . . . . . . . . . . . . . 16
185 inss2 3478 . . . . . . . . . . . . . . . . . 18
186 resmpt 5103 . . . . . . . . . . . . . . . . . 18
187185, 186ax-mp 8 . . . . . . . . . . . . . . . . 17
188187rneqi 5008 . . . . . . . . . . . . . . . 16
189184, 188eqtri 2386 . . . . . . . . . . . . . . 15
190189sseq1i 3288 . . . . . . . . . . . . . 14
191 dfss3 3256 . . . . . . . . . . . . . 14
192190, 191bitri 240 . . . . . . . . . . . . 13
19312adantr 451 . . . . . . . . . . . . . . . 16
194 ssralv 3323 . . . . . . . . . . . . . . . 16
195185, 193, 194mpsyl 59 . . . . . . . . . . . . . . 15
196 eqid 2366 . . . . . . . . . . . . . . . 16
197 eleq1 2426 . . . . . . . . . . . . . . . 16
198196, 197ralrnmpt 5780 . . . . . . . . . . . . . . 15
199195, 198syl 15 . . . . . . . . . . . . . 14
200199biimpd 198 . . . . . . . . . . . . 13
201192, 200syl5bi 208 . . . . . . . . . . . 12
202 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . 24
20338ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . 26
204 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26
205203, 204sseldd 3267 . . . . . . . . . . . . . . . . . . . . . . . . 25
206 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . . 25
207 pnfge 10620 . . . . . . . . . . . . . . . . . . . . . . . . . 26
208205, 207syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25
209 simplrl 736 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
210209rexrd 9028 . . . . . . . . . . . . . . . . . . . . . . . . . 26
211210, 6, 65sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . 25
212205, 206, 208, 211mpbir3and 1136 . . . . . . . . . . . . . . . . . . . . . . . 24
213202, 212sseldd 3267 . . . . . . . . . . . . . . . . . . . . . . 23
21427ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . 25
215214sselda 3266 . . . . . . . . . . . . . . . . . . . . . . . 24
216215adantrr 697 . . . . . . . . . . . . . . . . . . . . . . 23
217 elin 3446 . . . . . . . . . . . . . . . . . . . . . . 23
218213, 216, 217sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . 22
219218ex 423 . . . . . . . . . . . . . . . . . . . . 21
220219imim1d 69 . . . . . . . . . . . . . . . . . . . 20
22121a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23
22277adantl 452 . . . . . . . . . . . . . . . . . . . . . . . 24
223222ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 23
22416ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . 23
22529ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . 25
226225r19.21bi 2726 . . . . . . . . . . . . . . . . . . . . . . . 24
227226adantrr 697 . . . . . . . . . . . . . . . . . . . . . . 23
228221, 223, 224, 227, 82syl22anc 1184 . . . . . . . . . . . . . . . . . . . . . 22
229227, 224, 85syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23
230229breq1d 4135 . . . . . . . . . . . . . . . . . . . . . 22
231228, 230bitrd 244 . . . . . . . . . . . . . . . . . . . . 21
232231pm5.74da 668 . . . . . . . . . . . . . . . . . . . 20
233220, 232sylibd 205 . . . . . . . . . . . . . . . . . . 19
234233exp4a 589 . . . . . . . . . . . . . . . . . 18
235234ralimdv2 2708 . . . . . . . . . . . . . . . . 17
236235imp 418 . . . . . . . . . . . . . . . 16
237236an32s 779 . . . . . . . . . . . . . . 15
238237expr 598 . . . . . . . . . . . . . 14
239238reximdva 2740 . . . . . . . . . . . . 13
240239ex 423 . . . . . . . . . . . 12
241201, 240syld 40 . . . . . . . . . . 11
242241com23 72 . . . . . . . . . 10
243183, 242syl5 28 . . . . . . . . 9 ordTop
244243impl 603 . . . . . . . 8 ordTop
245244expimpd 586 . . . . . . 7 ordTop
246245rexlimdva 2752 . . . . . 6 ordTop
247246adantlr 695 . . . . 5 ordTop
248179, 247mpd 14 . . . 4
249248ralrimiva 2711 . . 3
25029, 36, 16rlim2lt 12178 . . . 4