Metamath Proof Explorer


Theorem xrlimcnp

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +oo . Since any ~>r 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)

Ref Expression
Hypotheses xrlimcnp.a φA=B+∞
xrlimcnp.b φB
xrlimcnp.r φxAR
xrlimcnp.c x=+∞R=C
xrlimcnp.j J=TopOpenfld
xrlimcnp.k K=ordTop𝑡A
Assertion xrlimcnp φxBRCxARKCnPJ+∞

Proof

Step Hyp Ref Expression
1 xrlimcnp.a φA=B+∞
2 xrlimcnp.b φB
3 xrlimcnp.r φxAR
4 xrlimcnp.c x=+∞R=C
5 xrlimcnp.j J=TopOpenfld
6 xrlimcnp.k K=ordTop𝑡A
7 3 fmpttd φxAR:A
8 7 adantr φxBRCxAR:A
9 eqid xAR=xAR
10 ssun2 +∞B+∞
11 pnfex +∞V
12 11 snid +∞+∞
13 10 12 sselii +∞B+∞
14 13 1 eleqtrrid φ+∞A
15 4 eleq1d x=+∞RC
16 3 ralrimiva φxAR
17 15 16 14 rspcdva φC
18 9 4 14 17 fvmptd3 φxAR+∞=C
19 18 ad2antrr φxBRCyJxAR+∞=C
20 19 eleq1d φxBRCyJxAR+∞yCy
21 cnxmet abs∞Met
22 5 cnfldtopn J=MetOpenabs
23 22 mopni2 abs∞MetyJCyr+Cballabsry
24 21 23 mp3an1 yJCyr+Cballabsry
25 ssun1 BB+∞
26 25 1 sseqtrrid φBA
27 ssralv BAxARxBR
28 26 16 27 sylc φxBR
29 28 ad2antrr φxBRCr+CballabsryxBR
30 simprl φxBRCr+Cballabsryr+
31 simplr φxBRCr+CballabsryxBRC
32 29 30 31 rlimi φxBRCr+CballabsrykxBkxRC<r
33 letop ordTopTop
34 ressxr *
35 2 34 sstrdi φB*
36 pnfxr +∞*
37 36 a1i φ+∞*
38 37 snssd φ+∞*
39 35 38 unssd φB+∞*
40 1 39 eqsstrd φA*
41 xrex *V
42 41 ssex A*AV
43 40 42 syl φAV
44 43 ad2antrr φr+CballabsrykxBkxRC<rAV
45 iocpnfordt k+∞ordTop
46 45 a1i φr+CballabsrykxBkxRC<rk+∞ordTop
47 elrestr ordTopTopAVk+∞ordTopk+∞AordTop𝑡A
48 33 44 46 47 mp3an2i φr+CballabsrykxBkxRC<rk+∞AordTop𝑡A
49 48 6 eleqtrrdi φr+CballabsrykxBkxRC<rk+∞AK
50 simprl φr+CballabsrykxBkxRC<rk
51 50 rexrd φr+CballabsrykxBkxRC<rk*
52 36 a1i φr+CballabsrykxBkxRC<r+∞*
53 50 ltpnfd φr+CballabsrykxBkxRC<rk<+∞
54 ubioc1 k*+∞*k<+∞+∞k+∞
55 51 52 53 54 syl3anc φr+CballabsrykxBkxRC<r+∞k+∞
56 14 ad2antrr φr+CballabsrykxBkxRC<r+∞A
57 55 56 elind φr+CballabsrykxBkxRC<r+∞k+∞A
58 simplr φr+CballabsrykxBk
59 58 rexrd φr+CballabsrykxBk*
60 elioc1 k*+∞*xk+∞x*k<xx+∞
61 59 36 60 sylancl φr+CballabsrykxBxk+∞x*k<xx+∞
62 simp2 x*k<xx+∞k<x
63 61 62 syl6bi φr+CballabsrykxBxk+∞k<x
64 2 ad2antrr φr+CballabsrykB
65 64 sselda φr+CballabsrykxBx
66 ltle kxk<xkx
67 58 65 66 syl2anc φr+CballabsrykxBk<xkx
68 63 67 syld φr+CballabsrykxBxk+∞kx
69 21 a1i φr+CballabsrykxBabs∞Met
70 simprl φr+Cballabsryr+
71 70 ad2antrr φr+CballabsrykxBr+
72 rpxr r+r*
73 71 72 syl φr+CballabsrykxBr*
74 17 ad3antrrr φr+CballabsrykxBC
75 28 ad2antrr φr+CballabsrykxBR
76 75 r19.21bi φr+CballabsrykxBR
77 elbl3 abs∞Metr*CRRCballabsrRabsC<r
78 69 73 74 76 77 syl22anc φr+CballabsrykxBRCballabsrRabsC<r
79 eqid abs=abs
80 79 cnmetdval RCRabsC=RC
81 76 74 80 syl2anc φr+CballabsrykxBRabsC=RC
82 81 breq1d φr+CballabsrykxBRabsC<rRC<r
83 78 82 bitrd φr+CballabsrykxBRCballabsrRC<r
84 83 biimprd φr+CballabsrykxBRC<rRCballabsr
85 68 84 imim12d φr+CballabsrykxBkxRC<rxk+∞RCballabsr
86 85 ralimdva φr+CballabsrykxBkxRC<rxBxk+∞RCballabsr
87 86 impr φr+CballabsrykxBkxRC<rxBxk+∞RCballabsr
88 17 ad2antrr φr+CballabsrykxBkxRC<rC
89 simplrl φr+CballabsrykxBkxRC<rr+
90 blcntr abs∞MetCr+CCballabsr
91 21 88 89 90 mp3an2i φr+CballabsrykxBkxRC<rCCballabsr
92 91 a1d φr+CballabsrykxBkxRC<r+∞k+∞CCballabsr
93 eleq1 x=+∞xk+∞+∞k+∞
94 4 eleq1d x=+∞RCballabsrCCballabsr
95 93 94 imbi12d x=+∞xk+∞RCballabsr+∞k+∞CCballabsr
96 11 95 ralsn x+∞xk+∞RCballabsr+∞k+∞CCballabsr
97 92 96 sylibr φr+CballabsrykxBkxRC<rx+∞xk+∞RCballabsr
98 ralunb xB+∞xk+∞RCballabsrxBxk+∞RCballabsrx+∞xk+∞RCballabsr
99 87 97 98 sylanbrc φr+CballabsrykxBkxRC<rxB+∞xk+∞RCballabsr
100 1 ad2antrr φr+CballabsrykxBkxRC<rA=B+∞
101 100 raleqdv φr+CballabsrykxBkxRC<rxAxk+∞RCballabsrxB+∞xk+∞RCballabsr
102 99 101 mpbird φr+CballabsrykxBkxRC<rxAxk+∞RCballabsr
103 ss2rab xA|xk+∞xA|RCballabsrxAxk+∞RCballabsr
104 102 103 sylibr φr+CballabsrykxBkxRC<rxA|xk+∞xA|RCballabsr
105 incom k+∞A=Ak+∞
106 dfin5 Ak+∞=xA|xk+∞
107 105 106 eqtri k+∞A=xA|xk+∞
108 9 mptpreima xAR-1Cballabsr=xA|RCballabsr
109 104 107 108 3sstr4g φr+CballabsrykxBkxRC<rk+∞AxAR-1Cballabsr
110 funmpt FunxAR
111 inss2 k+∞AA
112 7 ad2antrr φr+CballabsrykxBkxRC<rxAR:A
113 112 fdmd φr+CballabsrykxBkxRC<rdomxAR=A
114 111 113 sseqtrrid φr+CballabsrykxBkxRC<rk+∞AdomxAR
115 funimass3 FunxARk+∞AdomxARxARk+∞ACballabsrk+∞AxAR-1Cballabsr
116 110 114 115 sylancr φr+CballabsrykxBkxRC<rxARk+∞ACballabsrk+∞AxAR-1Cballabsr
117 109 116 mpbird φr+CballabsrykxBkxRC<rxARk+∞ACballabsr
118 simplrr φr+CballabsrykxBkxRC<rCballabsry
119 117 118 sstrd φr+CballabsrykxBkxRC<rxARk+∞Ay
120 eleq2 z=k+∞A+∞z+∞k+∞A
121 imaeq2 z=k+∞AxARz=xARk+∞A
122 121 sseq1d z=k+∞AxARzyxARk+∞Ay
123 120 122 anbi12d z=k+∞A+∞zxARzy+∞k+∞AxARk+∞Ay
124 123 rspcev k+∞AK+∞k+∞AxARk+∞AyzK+∞zxARzy
125 49 57 119 124 syl12anc φr+CballabsrykxBkxRC<rzK+∞zxARzy
126 125 rexlimdvaa φr+CballabsrykxBkxRC<rzK+∞zxARzy
127 126 adantlr φxBRCr+CballabsrykxBkxRC<rzK+∞zxARzy
128 32 127 mpd φxBRCr+CballabsryzK+∞zxARzy
129 128 rexlimdvaa φxBRCr+CballabsryzK+∞zxARzy
130 24 129 syl5 φxBRCyJCyzK+∞zxARzy
131 130 expdimp φxBRCyJCyzK+∞zxARzy
132 20 131 sylbid φxBRCyJxAR+∞yzK+∞zxARzy
133 132 ralrimiva φxBRCyJxAR+∞yzK+∞zxARzy
134 letopon ordTopTopOn*
135 resttopon ordTopTopOn*A*ordTop𝑡ATopOnA
136 134 40 135 sylancr φordTop𝑡ATopOnA
137 6 136 eqeltrid φKTopOnA
138 5 cnfldtopon JTopOn
139 138 a1i φJTopOn
140 iscnp KTopOnAJTopOn+∞AxARKCnPJ+∞xAR:AyJxAR+∞yzK+∞zxARzy
141 137 139 14 140 syl3anc φxARKCnPJ+∞xAR:AyJxAR+∞yzK+∞zxARzy
142 141 adantr φxBRCxARKCnPJ+∞xAR:AyJxAR+∞yzK+∞zxARzy
143 8 133 142 mpbir2and φxBRCxARKCnPJ+∞
144 simplr φxARKCnPJ+∞r+xARKCnPJ+∞
145 17 ad2antrr φxARKCnPJ+∞r+C
146 72 adantl φxARKCnPJ+∞r+r*
147 22 blopn abs∞MetCr*CballabsrJ
148 21 145 146 147 mp3an2i φxARKCnPJ+∞r+CballabsrJ
149 18 ad2antrr φxARKCnPJ+∞r+xAR+∞=C
150 simpr φxARKCnPJ+∞r+r+
151 21 145 150 90 mp3an2i φxARKCnPJ+∞r+CCballabsr
152 149 151 eqeltrd φxARKCnPJ+∞r+xAR+∞Cballabsr
153 cnpimaex xARKCnPJ+∞CballabsrJxAR+∞CballabsrzK+∞zxARzCballabsr
154 144 148 152 153 syl3anc φxARKCnPJ+∞r+zK+∞zxARzCballabsr
155 vex wV
156 155 inex1 wAV
157 156 a1i φxARKCnPJ+∞r+wordTopwAV
158 6 eleq2i zKzordTop𝑡A
159 43 ad2antrr φxARKCnPJ+∞r+AV
160 elrest ordTopTopAVzordTop𝑡AwordTopz=wA
161 33 159 160 sylancr φxARKCnPJ+∞r+zordTop𝑡AwordTopz=wA
162 158 161 bitrid φxARKCnPJ+∞r+zKwordTopz=wA
163 eleq2 z=wA+∞z+∞wA
164 imaeq2 z=wAxARz=xARwA
165 164 sseq1d z=wAxARzCballabsrxARwACballabsr
166 163 165 anbi12d z=wA+∞zxARzCballabsr+∞wAxARwACballabsr
167 166 adantl φxARKCnPJ+∞r+z=wA+∞zxARzCballabsr+∞wAxARwACballabsr
168 157 162 167 rexxfr2d φxARKCnPJ+∞r+zK+∞zxARzCballabsrwordTop+∞wAxARwACballabsr
169 154 168 mpbid φxARKCnPJ+∞r+wordTop+∞wAxARwACballabsr
170 elinel1 +∞wA+∞w
171 pnfnei wordTop+∞wkk+∞w
172 170 171 sylan2 wordTop+∞wAkk+∞w
173 df-ima xARwA=ranxARwA
174 inss2 wAA
175 resmpt wAAxARwA=xwAR
176 174 175 ax-mp xARwA=xwAR
177 176 rneqi ranxARwA=ranxwAR
178 173 177 eqtri xARwA=ranxwAR
179 178 sseq1i xARwACballabsrranxwARCballabsr
180 dfss3 ranxwARCballabsrzranxwARzCballabsr
181 179 180 bitri xARwACballabsrzranxwARzCballabsr
182 16 adantr φr+xAR
183 ssralv wAAxARxwAR
184 174 182 183 mpsyl φr+xwAR
185 eqid xwAR=xwAR
186 eleq1 z=RzCballabsrRCballabsr
187 185 186 ralrnmptw xwARzranxwARzCballabsrxwARCballabsr
188 184 187 syl φr+zranxwARzCballabsrxwARCballabsr
189 188 biimpd φr+zranxwARzCballabsrxwARCballabsr
190 181 189 biimtrid φr+xARwACballabsrxwARCballabsr
191 simplrr φr+kk+∞wxBk<xk+∞w
192 35 ad3antrrr φr+kk+∞wxBk<xB*
193 simprl φr+kk+∞wxBk<xxB
194 192 193 sseldd φr+kk+∞wxBk<xx*
195 simprr φr+kk+∞wxBk<xk<x
196 pnfge x*x+∞
197 194 196 syl φr+kk+∞wxBk<xx+∞
198 simplrl φr+kk+∞wxBk<xk
199 198 rexrd φr+kk+∞wxBk<xk*
200 199 36 60 sylancl φr+kk+∞wxBk<xxk+∞x*k<xx+∞
201 194 195 197 200 mpbir3and φr+kk+∞wxBk<xxk+∞
202 191 201 sseldd φr+kk+∞wxBk<xxw
203 26 ad2antrr φr+kk+∞wBA
204 203 sselda φr+kk+∞wxBxA
205 204 adantrr φr+kk+∞wxBk<xxA
206 202 205 elind φr+kk+∞wxBk<xxwA
207 206 ex φr+kk+∞wxBk<xxwA
208 207 imim1d φr+kk+∞wxwARCballabsrxBk<xRCballabsr
209 21 a1i φr+kk+∞wxBk<xabs∞Met
210 72 adantl φr+r*
211 210 ad2antrr φr+kk+∞wxBk<xr*
212 17 ad3antrrr φr+kk+∞wxBk<xC
213 28 ad2antrr φr+kk+∞wxBR
214 213 r19.21bi φr+kk+∞wxBR
215 214 adantrr φr+kk+∞wxBk<xR
216 209 211 212 215 77 syl22anc φr+kk+∞wxBk<xRCballabsrRabsC<r
217 215 212 80 syl2anc φr+kk+∞wxBk<xRabsC=RC
218 217 breq1d φr+kk+∞wxBk<xRabsC<rRC<r
219 216 218 bitrd φr+kk+∞wxBk<xRCballabsrRC<r
220 219 pm5.74da φr+kk+∞wxBk<xRCballabsrxBk<xRC<r
221 208 220 sylibd φr+kk+∞wxwARCballabsrxBk<xRC<r
222 221 exp4a φr+kk+∞wxwARCballabsrxBk<xRC<r
223 222 ralimdv2 φr+kk+∞wxwARCballabsrxBk<xRC<r
224 223 imp φr+kk+∞wxwARCballabsrxBk<xRC<r
225 224 an32s φr+xwARCballabsrkk+∞wxBk<xRC<r
226 225 expr φr+xwARCballabsrkk+∞wxBk<xRC<r
227 226 reximdva φr+xwARCballabsrkk+∞wkxBk<xRC<r
228 227 ex φr+xwARCballabsrkk+∞wkxBk<xRC<r
229 190 228 syld φr+xARwACballabsrkk+∞wkxBk<xRC<r
230 229 com23 φr+kk+∞wxARwACballabsrkxBk<xRC<r
231 172 230 syl5 φr+wordTop+∞wAxARwACballabsrkxBk<xRC<r
232 231 impl φr+wordTop+∞wAxARwACballabsrkxBk<xRC<r
233 232 expimpd φr+wordTop+∞wAxARwACballabsrkxBk<xRC<r
234 233 rexlimdva φr+wordTop+∞wAxARwACballabsrkxBk<xRC<r
235 234 adantlr φxARKCnPJ+∞r+wordTop+∞wAxARwACballabsrkxBk<xRC<r
236 169 235 mpd φxARKCnPJ+∞r+kxBk<xRC<r
237 236 ralrimiva φxARKCnPJ+∞r+kxBk<xRC<r
238 28 2 17 rlim2lt φxBRCr+kxBk<xRC<r
239 238 adantr φxARKCnPJ+∞xBRCr+kxBk<xRC<r
240 237 239 mpbird φxARKCnPJ+∞xBRC
241 143 240 impbida φxBRCxARKCnPJ+∞