Metamath Proof Explorer


Theorem rlimcnp3

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 rlimcnp3.c φC
rlimcnp3.r φy+S
rlimcnp3.s y=1xS=R
rlimcnp3.j J=TopOpenfld
rlimcnp3.k K=J𝑡0+∞
Assertion rlimcnp3 φy+SCx0+∞ifx=0CRKCnPJ0

Proof

Step Hyp Ref Expression
1 rlimcnp3.c φC
2 rlimcnp3.r φy+S
3 rlimcnp3.s y=1xS=R
4 rlimcnp3.j J=TopOpenfld
5 rlimcnp3.k K=J𝑡0+∞
6 ssidd φ0+∞0+∞
7 0e0icopnf 00+∞
8 7 a1i φ00+∞
9 rpssre +
10 9 a1i φ+
11 simpr φy+y+
12 rpreccl y+1y+
13 12 adantl φy+1y+
14 13 rpred φy+1y
15 13 rpge0d φy+01y
16 elrege0 1y0+∞1y01y
17 14 15 16 sylanbrc φy+1y0+∞
18 11 17 2thd φy+y+1y0+∞
19 6 8 10 1 2 18 3 4 5 rlimcnp2 φy+SCx0+∞ifx=0CRKCnPJ0