# Metamath Proof Explorer

## Theorem rlimcnp2

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the function S ( y ) = R ( 1 / y ) at zero. (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypotheses rlimcnp2.a ${⊢}{\phi }\to {A}\subseteq \left[0,\mathrm{+\infty }\right)$
rlimcnp2.0 ${⊢}{\phi }\to 0\in {A}$
rlimcnp2.b ${⊢}{\phi }\to {B}\subseteq ℝ$
rlimcnp2.c ${⊢}{\phi }\to {C}\in ℂ$
rlimcnp2.r ${⊢}\left({\phi }\wedge {y}\in {B}\right)\to {S}\in ℂ$
rlimcnp2.d ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\right)\to \left({y}\in {B}↔\frac{1}{{y}}\in {A}\right)$
rlimcnp2.s ${⊢}{y}=\frac{1}{{x}}\to {S}={R}$
rlimcnp2.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
rlimcnp2.k ${⊢}{K}={J}{↾}_{𝑡}{A}$
Assertion rlimcnp2

### Proof

Step Hyp Ref Expression
1 rlimcnp2.a ${⊢}{\phi }\to {A}\subseteq \left[0,\mathrm{+\infty }\right)$
2 rlimcnp2.0 ${⊢}{\phi }\to 0\in {A}$
3 rlimcnp2.b ${⊢}{\phi }\to {B}\subseteq ℝ$
4 rlimcnp2.c ${⊢}{\phi }\to {C}\in ℂ$
5 rlimcnp2.r ${⊢}\left({\phi }\wedge {y}\in {B}\right)\to {S}\in ℂ$
6 rlimcnp2.d ${⊢}\left({\phi }\wedge {y}\in {ℝ}^{+}\right)\to \left({y}\in {B}↔\frac{1}{{y}}\in {A}\right)$
7 rlimcnp2.s ${⊢}{y}=\frac{1}{{x}}\to {S}={R}$
8 rlimcnp2.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
9 rlimcnp2.k ${⊢}{K}={J}{↾}_{𝑡}{A}$
10 inss1 ${⊢}{B}\cap \left[1,\mathrm{+\infty }\right)\subseteq {B}$
11 resmpt ${⊢}{B}\cap \left[1,\mathrm{+\infty }\right)\subseteq {B}\to {\left({y}\in {B}⟼{S}\right)↾}_{\left({B}\cap \left[1,\mathrm{+\infty }\right)\right)}=\left({y}\in \left({B}\cap \left[1,\mathrm{+\infty }\right)\right)⟼{S}\right)$
12 10 11 mp1i ${⊢}{\phi }\to {\left({y}\in {B}⟼{S}\right)↾}_{\left({B}\cap \left[1,\mathrm{+\infty }\right)\right)}=\left({y}\in \left({B}\cap \left[1,\mathrm{+\infty }\right)\right)⟼{S}\right)$
13 0xr ${⊢}0\in {ℝ}^{*}$
14 0lt1 ${⊢}0<1$
15 df-ioo ${⊢}\left(.\right)=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}<{z}\wedge {z}<{y}\right)\right\}\right)$
16 df-ico ${⊢}\left[.\right)=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
17 xrltletr ${⊢}\left(0\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\left(0<1\wedge 1\le {w}\right)\to 0<{w}\right)$
18 15 16 17 ixxss1 ${⊢}\left(0\in {ℝ}^{*}\wedge 0<1\right)\to \left[1,\mathrm{+\infty }\right)\subseteq \left(0,\mathrm{+\infty }\right)$
19 13 14 18 mp2an ${⊢}\left[1,\mathrm{+\infty }\right)\subseteq \left(0,\mathrm{+\infty }\right)$
20 ioorp ${⊢}\left(0,\mathrm{+\infty }\right)={ℝ}^{+}$
21 19 20 sseqtri ${⊢}\left[1,\mathrm{+\infty }\right)\subseteq {ℝ}^{+}$
22 sslin ${⊢}\left[1,\mathrm{+\infty }\right)\subseteq {ℝ}^{+}\to {B}\cap \left[1,\mathrm{+\infty }\right)\subseteq {B}\cap {ℝ}^{+}$
23 21 22 ax-mp ${⊢}{B}\cap \left[1,\mathrm{+\infty }\right)\subseteq {B}\cap {ℝ}^{+}$
24 resmpt ${⊢}{B}\cap \left[1,\mathrm{+\infty }\right)\subseteq {B}\cap {ℝ}^{+}\to {\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)↾}_{\left({B}\cap \left[1,\mathrm{+\infty }\right)\right)}=\left({y}\in \left({B}\cap \left[1,\mathrm{+\infty }\right)\right)⟼{S}\right)$
25 23 24 mp1i ${⊢}{\phi }\to {\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)↾}_{\left({B}\cap \left[1,\mathrm{+\infty }\right)\right)}=\left({y}\in \left({B}\cap \left[1,\mathrm{+\infty }\right)\right)⟼{S}\right)$
26 12 25 eqtr4d ${⊢}{\phi }\to {\left({y}\in {B}⟼{S}\right)↾}_{\left({B}\cap \left[1,\mathrm{+\infty }\right)\right)}={\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)↾}_{\left({B}\cap \left[1,\mathrm{+\infty }\right)\right)}$
27 resres ${⊢}{\left({\left({y}\in {B}⟼{S}\right)↾}_{{B}}\right)↾}_{\left[1,\mathrm{+\infty }\right)}={\left({y}\in {B}⟼{S}\right)↾}_{\left({B}\cap \left[1,\mathrm{+\infty }\right)\right)}$
28 resres ${⊢}{\left({\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)↾}_{{B}}\right)↾}_{\left[1,\mathrm{+\infty }\right)}={\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)↾}_{\left({B}\cap \left[1,\mathrm{+\infty }\right)\right)}$
29 26 27 28 3eqtr4g ${⊢}{\phi }\to {\left({\left({y}\in {B}⟼{S}\right)↾}_{{B}}\right)↾}_{\left[1,\mathrm{+\infty }\right)}={\left({\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)↾}_{{B}}\right)↾}_{\left[1,\mathrm{+\infty }\right)}$
30 5 fmpttd ${⊢}{\phi }\to \left({y}\in {B}⟼{S}\right):{B}⟶ℂ$
31 30 ffnd ${⊢}{\phi }\to \left({y}\in {B}⟼{S}\right)Fn{B}$
32 fnresdm ${⊢}\left({y}\in {B}⟼{S}\right)Fn{B}\to {\left({y}\in {B}⟼{S}\right)↾}_{{B}}=\left({y}\in {B}⟼{S}\right)$
33 31 32 syl ${⊢}{\phi }\to {\left({y}\in {B}⟼{S}\right)↾}_{{B}}=\left({y}\in {B}⟼{S}\right)$
34 33 reseq1d ${⊢}{\phi }\to {\left({\left({y}\in {B}⟼{S}\right)↾}_{{B}}\right)↾}_{\left[1,\mathrm{+\infty }\right)}={\left({y}\in {B}⟼{S}\right)↾}_{\left[1,\mathrm{+\infty }\right)}$
35 elinel1 ${⊢}{y}\in \left({B}\cap {ℝ}^{+}\right)\to {y}\in {B}$
36 35 5 sylan2 ${⊢}\left({\phi }\wedge {y}\in \left({B}\cap {ℝ}^{+}\right)\right)\to {S}\in ℂ$
37 36 fmpttd ${⊢}{\phi }\to \left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right):{B}\cap {ℝ}^{+}⟶ℂ$
38 frel ${⊢}\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right):{B}\cap {ℝ}^{+}⟶ℂ\to \mathrm{Rel}\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)$
39 37 38 syl ${⊢}{\phi }\to \mathrm{Rel}\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)$
40 eqid ${⊢}\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)=\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)$
41 40 36 dmmptd ${⊢}{\phi }\to \mathrm{dom}\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)={B}\cap {ℝ}^{+}$
42 inss1 ${⊢}{B}\cap {ℝ}^{+}\subseteq {B}$
43 41 42 eqsstrdi ${⊢}{\phi }\to \mathrm{dom}\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)\subseteq {B}$
44 relssres ${⊢}\left(\mathrm{Rel}\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)\wedge \mathrm{dom}\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)\subseteq {B}\right)\to {\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)↾}_{{B}}=\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)$
45 39 43 44 syl2anc ${⊢}{\phi }\to {\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)↾}_{{B}}=\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)$
46 45 reseq1d ${⊢}{\phi }\to {\left({\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)↾}_{{B}}\right)↾}_{\left[1,\mathrm{+\infty }\right)}={\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)↾}_{\left[1,\mathrm{+\infty }\right)}$
47 29 34 46 3eqtr3d ${⊢}{\phi }\to {\left({y}\in {B}⟼{S}\right)↾}_{\left[1,\mathrm{+\infty }\right)}={\left({y}\in \left({B}\cap {ℝ}^{+}\right)⟼{S}\right)↾}_{\left[1,\mathrm{+\infty }\right)}$
48 47 breq1d
49 1red ${⊢}{\phi }\to 1\in ℝ$
50 30 3 49 rlimresb
51 42 3 sstrid ${⊢}{\phi }\to {B}\cap {ℝ}^{+}\subseteq ℝ$
52 37 51 49 rlimresb
53 48 50 52 3bitr4d
54 inss2 ${⊢}{B}\cap {ℝ}^{+}\subseteq {ℝ}^{+}$
55 54 a1i ${⊢}{\phi }\to {B}\cap {ℝ}^{+}\subseteq {ℝ}^{+}$
56 55 sselda ${⊢}\left({\phi }\wedge {y}\in \left({B}\cap {ℝ}^{+}\right)\right)\to {y}\in {ℝ}^{+}$
57 56 rpreccld ${⊢}\left({\phi }\wedge {y}\in \left({B}\cap {ℝ}^{+}\right)\right)\to \frac{1}{{y}}\in {ℝ}^{+}$
58 57 rpne0d ${⊢}\left({\phi }\wedge {y}\in \left({B}\cap {ℝ}^{+}\right)\right)\to \frac{1}{{y}}\ne 0$
59 58 neneqd ${⊢}\left({\phi }\wedge {y}\in \left({B}\cap {ℝ}^{+}\right)\right)\to ¬\frac{1}{{y}}=0$
60 59 iffalsed
61 oveq2 ${⊢}{x}=\frac{1}{{y}}\to \frac{1}{{x}}=\frac{1}{\frac{1}{{y}}}$
62 rpcnne0 ${⊢}{y}\in {ℝ}^{+}\to \left({y}\in ℂ\wedge {y}\ne 0\right)$
63 recrec ${⊢}\left({y}\in ℂ\wedge {y}\ne 0\right)\to \frac{1}{\frac{1}{{y}}}={y}$
64 56 62 63 3syl ${⊢}\left({\phi }\wedge {y}\in \left({B}\cap {ℝ}^{+}\right)\right)\to \frac{1}{\frac{1}{{y}}}={y}$
65 61 64 sylan9eqr ${⊢}\left(\left({\phi }\wedge {y}\in \left({B}\cap {ℝ}^{+}\right)\right)\wedge {x}=\frac{1}{{y}}\right)\to \frac{1}{{x}}={y}$
66 65 eqcomd ${⊢}\left(\left({\phi }\wedge {y}\in \left({B}\cap {ℝ}^{+}\right)\right)\wedge {x}=\frac{1}{{y}}\right)\to {y}=\frac{1}{{x}}$
67 66 7 syl ${⊢}\left(\left({\phi }\wedge {y}\in \left({B}\cap {ℝ}^{+}\right)\right)\wedge {x}=\frac{1}{{y}}\right)\to {S}={R}$
68 67 eqcomd ${⊢}\left(\left({\phi }\wedge {y}\in \left({B}\cap {ℝ}^{+}\right)\right)\wedge {x}=\frac{1}{{y}}\right)\to {R}={S}$
69 57 68 csbied
70 60 69 eqtrd
71 70 mpteq2dva
72 71 breq1d
73 4 ad2antrr ${⊢}\left(\left({\phi }\wedge {w}\in {A}\right)\wedge {w}=0\right)\to {C}\in ℂ$
74 1 sselda ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to {w}\in \left[0,\mathrm{+\infty }\right)$
75 0re ${⊢}0\in ℝ$
76 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
77 elico2 ${⊢}\left(0\in ℝ\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left({w}\in \left[0,\mathrm{+\infty }\right)↔\left({w}\in ℝ\wedge 0\le {w}\wedge {w}<\mathrm{+\infty }\right)\right)$
78 75 76 77 mp2an ${⊢}{w}\in \left[0,\mathrm{+\infty }\right)↔\left({w}\in ℝ\wedge 0\le {w}\wedge {w}<\mathrm{+\infty }\right)$
79 74 78 sylib ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \left({w}\in ℝ\wedge 0\le {w}\wedge {w}<\mathrm{+\infty }\right)$
80 79 simp1d ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to {w}\in ℝ$
81 80 adantr ${⊢}\left(\left({\phi }\wedge {w}\in {A}\right)\wedge ¬{w}=0\right)\to {w}\in ℝ$
82 79 simp2d ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to 0\le {w}$
83 leloe ${⊢}\left(0\in ℝ\wedge {w}\in ℝ\right)\to \left(0\le {w}↔\left(0<{w}\vee 0={w}\right)\right)$
84 75 80 83 sylancr ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \left(0\le {w}↔\left(0<{w}\vee 0={w}\right)\right)$
85 82 84 mpbid ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \left(0<{w}\vee 0={w}\right)$
86 85 ord ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \left(¬0<{w}\to 0={w}\right)$
87 eqcom ${⊢}0={w}↔{w}=0$
88 86 87 syl6ib ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \left(¬0<{w}\to {w}=0\right)$
89 88 con1d ${⊢}\left({\phi }\wedge {w}\in {A}\right)\to \left(¬{w}=0\to 0<{w}\right)$
90 89 imp ${⊢}\left(\left({\phi }\wedge {w}\in {A}\right)\wedge ¬{w}=0\right)\to 0<{w}$
91 81 90 elrpd ${⊢}\left(\left({\phi }\wedge {w}\in {A}\right)\wedge ¬{w}=0\right)\to {w}\in {ℝ}^{+}$
92 rpcnne0 ${⊢}{w}\in {ℝ}^{+}\to \left({w}\in ℂ\wedge {w}\ne 0\right)$
93 recrec ${⊢}\left({w}\in ℂ\wedge {w}\ne 0\right)\to \frac{1}{\frac{1}{{w}}}={w}$
94 92 93 syl ${⊢}{w}\in {ℝ}^{+}\to \frac{1}{\frac{1}{{w}}}={w}$
95 91 94 syl ${⊢}\left(\left({\phi }\wedge {w}\in {A}\right)\wedge ¬{w}=0\right)\to \frac{1}{\frac{1}{{w}}}={w}$
96 95 csbeq1d
97 oveq2 ${⊢}{y}=\frac{1}{{w}}\to \frac{1}{{y}}=\frac{1}{\frac{1}{{w}}}$
98 97 csbeq1d
99 98 eleq1d
100 69 36 eqeltrd
101 100 ralrimiva
103 simplr ${⊢}\left(\left({\phi }\wedge {w}\in {A}\right)\wedge ¬{w}=0\right)\to {w}\in {A}$
104 simpll ${⊢}\left(\left({\phi }\wedge {w}\in {A}\right)\wedge ¬{w}=0\right)\to {\phi }$
105 eleq1 ${⊢}{y}=\frac{1}{{w}}\to \left({y}\in {B}↔\frac{1}{{w}}\in {B}\right)$
106 97 eleq1d ${⊢}{y}=\frac{1}{{w}}\to \left(\frac{1}{{y}}\in {A}↔\frac{1}{\frac{1}{{w}}}\in {A}\right)$
107 105 106 bibi12d ${⊢}{y}=\frac{1}{{w}}\to \left(\left({y}\in {B}↔\frac{1}{{y}}\in {A}\right)↔\left(\frac{1}{{w}}\in {B}↔\frac{1}{\frac{1}{{w}}}\in {A}\right)\right)$
108 6 ralrimiva ${⊢}{\phi }\to \forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}↔\frac{1}{{y}}\in {A}\right)$
109 108 adantr ${⊢}\left({\phi }\wedge {w}\in {ℝ}^{+}\right)\to \forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}↔\frac{1}{{y}}\in {A}\right)$
110 rpreccl ${⊢}{w}\in {ℝ}^{+}\to \frac{1}{{w}}\in {ℝ}^{+}$
111 110 adantl ${⊢}\left({\phi }\wedge {w}\in {ℝ}^{+}\right)\to \frac{1}{{w}}\in {ℝ}^{+}$
112 107 109 111 rspcdva ${⊢}\left({\phi }\wedge {w}\in {ℝ}^{+}\right)\to \left(\frac{1}{{w}}\in {B}↔\frac{1}{\frac{1}{{w}}}\in {A}\right)$
113 94 adantl ${⊢}\left({\phi }\wedge {w}\in {ℝ}^{+}\right)\to \frac{1}{\frac{1}{{w}}}={w}$
114 113 eleq1d ${⊢}\left({\phi }\wedge {w}\in {ℝ}^{+}\right)\to \left(\frac{1}{\frac{1}{{w}}}\in {A}↔{w}\in {A}\right)$
115 112 114 bitr2d ${⊢}\left({\phi }\wedge {w}\in {ℝ}^{+}\right)\to \left({w}\in {A}↔\frac{1}{{w}}\in {B}\right)$
116 104 91 115 syl2anc ${⊢}\left(\left({\phi }\wedge {w}\in {A}\right)\wedge ¬{w}=0\right)\to \left({w}\in {A}↔\frac{1}{{w}}\in {B}\right)$
117 103 116 mpbid ${⊢}\left(\left({\phi }\wedge {w}\in {A}\right)\wedge ¬{w}=0\right)\to \frac{1}{{w}}\in {B}$
118 91 rpreccld ${⊢}\left(\left({\phi }\wedge {w}\in {A}\right)\wedge ¬{w}=0\right)\to \frac{1}{{w}}\in {ℝ}^{+}$
119 117 118 elind ${⊢}\left(\left({\phi }\wedge {w}\in {A}\right)\wedge ¬{w}=0\right)\to \frac{1}{{w}}\in \left({B}\cap {ℝ}^{+}\right)$
120 99 102 119 rspcdva
121 96 120 eqeltrrd
122 73 121 ifclda
123 111 biantrud ${⊢}\left({\phi }\wedge {w}\in {ℝ}^{+}\right)\to \left(\frac{1}{{w}}\in {B}↔\left(\frac{1}{{w}}\in {B}\wedge \frac{1}{{w}}\in {ℝ}^{+}\right)\right)$
124 115 123 bitrd ${⊢}\left({\phi }\wedge {w}\in {ℝ}^{+}\right)\to \left({w}\in {A}↔\left(\frac{1}{{w}}\in {B}\wedge \frac{1}{{w}}\in {ℝ}^{+}\right)\right)$
125 elin ${⊢}\frac{1}{{w}}\in \left({B}\cap {ℝ}^{+}\right)↔\left(\frac{1}{{w}}\in {B}\wedge \frac{1}{{w}}\in {ℝ}^{+}\right)$
126 124 125 syl6bbr ${⊢}\left({\phi }\wedge {w}\in {ℝ}^{+}\right)\to \left({w}\in {A}↔\frac{1}{{w}}\in \left({B}\cap {ℝ}^{+}\right)\right)$
127 iftrue
128 eqeq1 ${⊢}{w}=\frac{1}{{y}}\to \left({w}=0↔\frac{1}{{y}}=0\right)$
129 csbeq1
130 128 129 ifbieq2d
131 1 2 55 122 126 127 130 8 9 rlimcnp
132 nfcv ${⊢}\underset{_}{Ⅎ}{w}\phantom{\rule{.4em}{0ex}}if\left({x}=0,{C},{R}\right)$
133 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{w}=0$
134 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
135 nfcsb1v
136 133 134 135 nfif
137 eqeq1 ${⊢}{x}={w}\to \left({x}=0↔{w}=0\right)$
138 csbeq1a
139 137 138 ifbieq2d
140 132 136 139 cbvmpt
141 140 eleq1i
142 131 141 syl6bbr
143 53 72 142 3bitr2d