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

Theorem xrlimcnp 20760
 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 2404 . . . . 5
31, 2fmptd 5852 . . . 4
5 ssun2 3471 . . . . . . . . . 10
6 pnfxr 10669 . . . . . . . . . . . 12
76elexi 2925 . . . . . . . . . . 11
87snid 3801 . . . . . . . . . 10
95, 8sselii 3305 . . . . . . . . 9
10 xrlimcnp.a . . . . . . . . 9
119, 10syl5eleqr 2491 . . . . . . . 8
121ralrimiva 2749 . . . . . . . . 9
13 xrlimcnp.c . . . . . . . . . . 11
1413eleq1d 2470 . . . . . . . . . 10
1514rspcv 3008 . . . . . . . . 9
1611, 12, 15sylc 58 . . . . . . . 8
1713, 2fvmptg 5763 . . . . . . . 8
1811, 16, 17syl2anc 643 . . . . . . 7
1918ad2antrr 707 . . . . . 6
2019eleq1d 2470 . . . . 5
21 cnxmet 18760 . . . . . . . 8
22 xrlimcnp.j . . . . . . . . . 10 fld
2322cnfldtopn 18769 . . . . . . . . 9
2423mopni2 18476 . . . . . . . 8
2521, 24mp3an1 1266 . . . . . . 7
26 ssun1 3470 . . . . . . . . . . . . 13
2726, 10syl5sseqr 3357 . . . . . . . . . . . 12
28 ssralv 3367 . . . . . . . . . . . 12
2927, 12, 28sylc 58 . . . . . . . . . . 11
3029ad2antrr 707 . . . . . . . . . 10
31 simprl 733 . . . . . . . . . 10
32 simplr 732 . . . . . . . . . 10
3330, 31, 32rlimi 12262 . . . . . . . . 9
34 letop 17224 . . . . . . . . . . . . . . 15 ordTop
3534a1i 11 . . . . . . . . . . . . . 14 ordTop
36 xrlimcnp.b . . . . . . . . . . . . . . . . . . 19
37 ressxr 9085 . . . . . . . . . . . . . . . . . . 19
3836, 37syl6ss 3320 . . . . . . . . . . . . . . . . . 18
396a1i 11 . . . . . . . . . . . . . . . . . . 19
4039snssd 3903 . . . . . . . . . . . . . . . . . 18
4138, 40unssd 3483 . . . . . . . . . . . . . . . . 17
4210, 41eqsstrd 3342 . . . . . . . . . . . . . . . 16
43 xrex 10565 . . . . . . . . . . . . . . . . 17
4443ssex 4307 . . . . . . . . . . . . . . . 16
4542, 44syl 16 . . . . . . . . . . . . . . 15
4645ad2antrr 707 . . . . . . . . . . . . . 14
47 iocpnfordt 17233 . . . . . . . . . . . . . . 15 ordTop
4847a1i 11 . . . . . . . . . . . . . 14 ordTop
49 elrestr 13611 . . . . . . . . . . . . . 14 ordTop ordTop ordTop t
5035, 46, 48, 49syl3anc 1184 . . . . . . . . . . . . 13 ordTop t
51 xrlimcnp.k . . . . . . . . . . . . 13 ordTop t
5250, 51syl6eleqr 2495 . . . . . . . . . . . 12
53 simprl 733 . . . . . . . . . . . . . . 15
5453rexrd 9090 . . . . . . . . . . . . . 14
556a1i 11 . . . . . . . . . . . . . 14
56 ltpnf 10677 . . . . . . . . . . . . . . 15
5753, 56syl 16 . . . . . . . . . . . . . 14
58 ubioc1 10921 . . . . . . . . . . . . . 14
5954, 55, 57, 58syl3anc 1184 . . . . . . . . . . . . 13
6011ad2antrr 707 . . . . . . . . . . . . 13
61 elin 3490 . . . . . . . . . . . . 13
6259, 60, 61sylanbrc 646 . . . . . . . . . . . 12
63 simplr 732 . . . . . . . . . . . . . . . . . . . . . . . . 25
6463rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . 24
65 elioc1 10914 . . . . . . . . . . . . . . . . . . . . . . . 24
6664, 6, 65sylancl 644 . . . . . . . . . . . . . . . . . . . . . . 23
67 simp2 958 . . . . . . . . . . . . . . . . . . . . . . 23
6866, 67syl6bi 220 . . . . . . . . . . . . . . . . . . . . . 22
6936ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . 24
7069sselda 3308 . . . . . . . . . . . . . . . . . . . . . . 23
71 ltle 9119 . . . . . . . . . . . . . . . . . . . . . . 23
7263, 70, 71syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
7368, 72syld 42 . . . . . . . . . . . . . . . . . . . . 21
7421a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
75 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7675ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25
77 rpxr 10575 . . . . . . . . . . . . . . . . . . . . . . . . 25
7876, 77syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
7916ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . 24
8029ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25
8180r19.21bi 2764 . . . . . . . . . . . . . . . . . . . . . . . 24
82 elbl3 18375 . . . . . . . . . . . . . . . . . . . . . . . 24
8374, 78, 79, 81, 82syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . 23
84 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8584cnmetdval 18758 . . . . . . . . . . . . . . . . . . . . . . . . 25
8681, 79, 85syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24
8786breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . 23
8883, 87bitrd 245 . . . . . . . . . . . . . . . . . . . . . 22
8988biimprd 215 . . . . . . . . . . . . . . . . . . . . 21
9073, 89imim12d 70 . . . . . . . . . . . . . . . . . . . 20
9190ralimdva 2744 . . . . . . . . . . . . . . . . . . 19
9291impr 603 . . . . . . . . . . . . . . . . . 18
9321a1i 11 . . . . . . . . . . . . . . . . . . . . 21
9416ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21
95 simplrl 737 . . . . . . . . . . . . . . . . . . . . 21
96 blcntr 18396 . . . . . . . . . . . . . . . . . . . . 21
9793, 94, 95, 96syl3anc 1184 . . . . . . . . . . . . . . . . . . . 20
9897a1d 23 . . . . . . . . . . . . . . . . . . 19
99 eleq1 2464 . . . . . . . . . . . . . . . . . . . . 21
10013eleq1d 2470 . . . . . . . . . . . . . . . . . . . . 21
10199, 100imbi12d 312 . . . . . . . . . . . . . . . . . . . 20
1027, 101ralsn 3809 . . . . . . . . . . . . . . . . . . 19
10398, 102sylibr 204 . . . . . . . . . . . . . . . . . 18
104 ralunb 3488 . . . . . . . . . . . . . . . . . 18
10592, 103, 104sylanbrc 646 . . . . . . . . . . . . . . . . 17
10610ad2antrr 707 . . . . . . . . . . . . . . . . . 18
107106raleqdv 2870 . . . . . . . . . . . . . . . . 17
108105, 107mpbird 224 . . . . . . . . . . . . . . . 16
109 ss2rab 3379 . . . . . . . . . . . . . . . 16
110108, 109sylibr 204 . . . . . . . . . . . . . . 15
111 incom 3493 . . . . . . . . . . . . . . . 16
112 dfin5 3288 . . . . . . . . . . . . . . . 16
113111, 112eqtri 2424 . . . . . . . . . . . . . . 15
1142mptpreima 5322 . . . . . . . . . . . . . . 15
115110, 113, 1143sstr4g 3349 . . . . . . . . . . . . . 14
116 funmpt 5448 . . . . . . . . . . . . . . 15
117 inss2 3522 . . . . . . . . . . . . . . . 16
1183ad2antrr 707 . . . . . . . . . . . . . . . . 17
119 fdm 5554 . . . . . . . . . . . . . . . . 17
120118, 119syl 16 . . . . . . . . . . . . . . . 16
121117, 120syl5sseqr 3357 . . . . . . . . . . . . . . 15
122 funimass3 5805 . . . . . . . . . . . . . . 15
123116, 121, 122sylancr 645 . . . . . . . . . . . . . 14
124115, 123mpbird 224 . . . . . . . . . . . . 13
125 simplrr 738 . . . . . . . . . . . . 13
126124, 125sstrd 3318 . . . . . . . . . . . 12
127 eleq2 2465 . . . . . . . . . . . . . 14
128 imaeq2 5158 . . . . . . . . . . . . . . 15
129128sseq1d 3335 . . . . . . . . . . . . . 14
130127, 129anbi12d 692 . . . . . . . . . . . . 13
131130rspcev 3012 . . . . . . . . . . . 12
13252, 62, 126, 131syl12anc 1182 . . . . . . . . . . 11
133132rexlimdvaa 2791 . . . . . . . . . 10
134133adantlr 696 . . . . . . . . 9
13533, 134mpd 15 . . . . . . . 8
136135rexlimdvaa 2791 . . . . . . 7
13725, 136syl5 30 . . . . . 6
138137expdimp 427 . . . . 5
13920, 138sylbid 207 . . . 4
140139ralrimiva 2749 . . 3
141 letopon 17223 . . . . . . 7 ordTop TopOn
142 resttopon 17179 . . . . . . 7 ordTop TopOn ordTop t TopOn
143141, 42, 142sylancr 645 . . . . . 6 ordTop t TopOn
14451, 143syl5eqel 2488 . . . . 5 TopOn
14522cnfldtopon 18770 . . . . . 6 TopOn
146145a1i 11 . . . . 5 TopOn
147 iscnp 17255 . . . . 5 TopOn TopOn
148144, 146, 11, 147syl3anc 1184 . . . 4
1504, 140, 149mpbir2and 889 . 2
151 simplr 732 . . . . . . 7
15221a1i 11 . . . . . . . 8
15316ad2antrr 707 . . . . . . . 8
15477adantl 453 . . . . . . . 8
15523blopn 18483 . . . . . . . 8
156152, 153, 154, 155syl3anc 1184 . . . . . . 7
15718ad2antrr 707 . . . . . . . 8
158 simpr 448 . . . . . . . . 9
159152, 153, 158, 96syl3anc 1184 . . . . . . . 8
160157, 159eqeltrd 2478 . . . . . . 7
161 cnpimaex 17274 . . . . . . 7
162151, 156, 160, 161syl3anc 1184 . . . . . 6
163 vex 2919 . . . . . . . . 9
164163inex1 4304 . . . . . . . 8
165164a1i 11 . . . . . . 7 ordTop
16651eleq2i 2468 . . . . . . . 8 ordTop t
16745ad2antrr 707 . . . . . . . . 9
168 elrest 13610 . . . . . . . . 9 ordTop ordTop t ordTop
16934, 167, 168sylancr 645 . . . . . . . 8 ordTop t ordTop
170166, 169syl5bb 249 . . . . . . 7 ordTop
171 eleq2 2465 . . . . . . . . 9
172 imaeq2 5158 . . . . . . . . . 10
173172sseq1d 3335 . . . . . . . . 9
174171, 173anbi12d 692 . . . . . . . 8
175174adantl 453 . . . . . . 7
176165, 170, 175rexxfr2d 4699 . . . . . 6 ordTop
177162, 176mpbid 202 . . . . 5 ordTop
178 inss1 3521 . . . . . . . . . . . 12
179178sseli 3304 . . . . . . . . . . 11
180 pnfnei 17238 . . . . . . . . . . 11 ordTop
181179, 180sylan2 461 . . . . . . . . . 10 ordTop
182 df-ima 4850 . . . . . . . . . . . . . . . 16
183 inss2 3522 . . . . . . . . . . . . . . . . . 18
184 resmpt 5150 . . . . . . . . . . . . . . . . . 18
185183, 184ax-mp 8 . . . . . . . . . . . . . . . . 17
186185rneqi 5055 . . . . . . . . . . . . . . . 16
187182, 186eqtri 2424 . . . . . . . . . . . . . . 15
188187sseq1i 3332 . . . . . . . . . . . . . 14
189 dfss3 3298 . . . . . . . . . . . . . 14
190188, 189bitri 241 . . . . . . . . . . . . 13
19112adantr 452 . . . . . . . . . . . . . . . 16
192 ssralv 3367 . . . . . . . . . . . . . . . 16
193183, 191, 192mpsyl 61 . . . . . . . . . . . . . . 15
194 eqid 2404 . . . . . . . . . . . . . . . 16
195 eleq1 2464 . . . . . . . . . . . . . . . 16
196194, 195ralrnmpt 5837 . . . . . . . . . . . . . . 15
197193, 196syl 16 . . . . . . . . . . . . . 14
198197biimpd 199 . . . . . . . . . . . . 13
199190, 198syl5bi 209 . . . . . . . . . . . 12
200 simplrr 738 . . . . . . . . . . . . . . . . . . . . . . . 24
20138ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26
202 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . 26
203201, 202sseldd 3309 . . . . . . . . . . . . . . . . . . . . . . . . 25
204 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . . 25
205 pnfge 10683 . . . . . . . . . . . . . . . . . . . . . . . . . 26
206203, 205syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
207 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
208207rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . . . 26
209208, 6, 65sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . 25
210203, 204, 206, 209mpbir3and 1137 . . . . . . . . . . . . . . . . . . . . . . . 24
211200, 210sseldd 3309 . . . . . . . . . . . . . . . . . . . . . . 23
21227ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25
213212sselda 3308 . . . . . . . . . . . . . . . . . . . . . . . 24
214213adantrr 698 . . . . . . . . . . . . . . . . . . . . . . 23
215 elin 3490 . . . . . . . . . . . . . . . . . . . . . . 23
216211, 214, 215sylanbrc 646 . . . . . . . . . . . . . . . . . . . . . 22
217216ex 424 . . . . . . . . . . . . . . . . . . . . 21
218217imim1d 71 . . . . . . . . . . . . . . . . . . . 20
21921a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
22077adantl 453 . . . . . . . . . . . . . . . . . . . . . . . 24
221220ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . 23
22216ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . 23
22329ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25
224223r19.21bi 2764 . . . . . . . . . . . . . . . . . . . . . . . 24
225224adantrr 698 . . . . . . . . . . . . . . . . . . . . . . 23
226219, 221, 222, 225, 82syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . 22
227225, 222, 85syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
228227breq1d 4182 . . . . . . . . . . . . . . . . . . . . . 22
229226, 228bitrd 245 . . . . . . . . . . . . . . . . . . . . 21
230229pm5.74da 669 . . . . . . . . . . . . . . . . . . . 20
231218, 230sylibd 206 . . . . . . . . . . . . . . . . . . 19
232231exp4a 590 . . . . . . . . . . . . . . . . . 18
233232ralimdv2 2746 . . . . . . . . . . . . . . . . 17
234233imp 419 . . . . . . . . . . . . . . . 16
235234an32s 780 . . . . . . . . . . . . . . 15
236235expr 599 . . . . . . . . . . . . . 14
237236reximdva 2778 . . . . . . . . . . . . 13
238237ex 424 . . . . . . . . . . . 12
239199, 238syld 42 . . . . . . . . . . 11
240239com23 74 . . . . . . . . . 10
241181, 240syl5 30 . . . . . . . . 9 ordTop
242241impl 604 . . . . . . . 8 ordTop
243242expimpd 587 . . . . . . 7 ordTop
244243rexlimdva 2790 . . . . . 6 ordTop
245244adantlr 696 . . . . 5 ordTop
246177, 245mpd 15 . . . 4
247246ralrimiva 2749 . . 3
24829, 36, 16rlim2lt 12246 . . . 4