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	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	rlimcnp3.r	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑆 ∈ ℂ )
	rlimcnp3.s	⊢ ( 𝑦 = ( 1 / 𝑥 ) → 𝑆 = 𝑅 )
	rlimcnp3.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
	rlimcnp3.k	⊢ 𝐾 = ( 𝐽 ↾t ( 0 [,) +∞ ) )
Assertion	rlimcnp3	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ+ ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ if ( 𝑥 = 0 , 𝐶 , 𝑅 ) ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rlimcnp3.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2		rlimcnp3.r	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑆 ∈ ℂ )
3		rlimcnp3.s	⊢ ( 𝑦 = ( 1 / 𝑥 ) → 𝑆 = 𝑅 )
4		rlimcnp3.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
5		rlimcnp3.k	⊢ 𝐾 = ( 𝐽 ↾t ( 0 [,) +∞ ) )
6		ssidd	⊢ ( 𝜑 → ( 0 [,) +∞ ) ⊆ ( 0 [,) +∞ ) )
7		0e0icopnf	⊢ 0 ∈ ( 0 [,) +∞ )
8	7	a1i	⊢ ( 𝜑 → 0 ∈ ( 0 [,) +∞ ) )
9		rpssre	⊢ ℝ+ ⊆ ℝ
10	9	a1i	⊢ ( 𝜑 → ℝ+ ⊆ ℝ )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 𝑦 ∈ ℝ+ )
12		rpreccl	⊢ ( 𝑦 ∈ ℝ+ → ( 1 / 𝑦 ) ∈ ℝ+ )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 1 / 𝑦 ) ∈ ℝ+ )
14	13	rpred	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 1 / 𝑦 ) ∈ ℝ )
15	13	rpge0d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → 0 ≤ ( 1 / 𝑦 ) )
16		elrege0	⊢ ( ( 1 / 𝑦 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 1 / 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝑦 ) ) )
17	14 15 16	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 1 / 𝑦 ) ∈ ( 0 [,) +∞ ) )
18	11 17	2thd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ+ ) → ( 𝑦 ∈ ℝ+ ↔ ( 1 / 𝑦 ) ∈ ( 0 [,) +∞ ) ) )
19	6 8 10 1 2 18 3 4 5	rlimcnp2	⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ+ ↦ 𝑆 ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ if ( 𝑥 = 0 , 𝐶 , 𝑅 ) ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ 0 ) ) )