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	|- ( ph -> C e. CC )
	rlimcnp3.r	|- ( ( ph /\ y e. RR+ ) -> S e. CC )
	rlimcnp3.s	|- ( y = ( 1 / x ) -> S = R )
	rlimcnp3.j	|- J = ( TopOpen ` CCfld )
	rlimcnp3.k	|- K = ( J |`t ( 0 [,) +oo ) )
Assertion	rlimcnp3	|- ( ph -> ( ( y e. RR+ |-> S ) ~~>r C <-> ( x e. ( 0 [,) +oo ) |-> if ( x = 0 , C , R ) ) e. ( ( K CnP J ) ` 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rlimcnp3.c	|- ( ph -> C e. CC )
2		rlimcnp3.r	|- ( ( ph /\ y e. RR+ ) -> S e. CC )
3		rlimcnp3.s	|- ( y = ( 1 / x ) -> S = R )
4		rlimcnp3.j	|- J = ( TopOpen ` CCfld )
5		rlimcnp3.k	|- K = ( J |`t ( 0 [,) +oo ) )
6		ssidd	|- ( ph -> ( 0 [,) +oo ) C_ ( 0 [,) +oo ) )
7		0e0icopnf	|- 0 e. ( 0 [,) +oo )
8	7	a1i	|- ( ph -> 0 e. ( 0 [,) +oo ) )
9		rpssre	|- RR+ C_ RR
10	9	a1i	|- ( ph -> RR+ C_ RR )
11		simpr	|- ( ( ph /\ y e. RR+ ) -> y e. RR+ )
12		rpreccl	|- ( y e. RR+ -> ( 1 / y ) e. RR+ )
13	12	adantl	|- ( ( ph /\ y e. RR+ ) -> ( 1 / y ) e. RR+ )
14	13	rpred	|- ( ( ph /\ y e. RR+ ) -> ( 1 / y ) e. RR )
15	13	rpge0d	|- ( ( ph /\ y e. RR+ ) -> 0 <_ ( 1 / y ) )
16		elrege0	|- ( ( 1 / y ) e. ( 0 [,) +oo ) <-> ( ( 1 / y ) e. RR /\ 0 <_ ( 1 / y ) ) )
17	14 15 16	sylanbrc	|- ( ( ph /\ y e. RR+ ) -> ( 1 / y ) e. ( 0 [,) +oo ) )
18	11 17	2thd	|- ( ( ph /\ y e. RR+ ) -> ( y e. RR+ <-> ( 1 / y ) e. ( 0 [,) +oo ) ) )
19	6 8 10 1 2 18 3 4 5	rlimcnp2	|- ( ph -> ( ( y e. RR+ |-> S ) ~~>r C <-> ( x e. ( 0 [,) +oo ) |-> if ( x = 0 , C , R ) ) e. ( ( K CnP J ) ` 0 ) ) )