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	$⊢ φ \to C \in ℂ$
		rlimcnp3.r	$⊢ (φ \land y \in ℝ^{+}) \to S \in ℂ$
		rlimcnp3.s	$⊢ y = \frac{1}{x} \to S = R$
		rlimcnp3.j	$⊢ J = TopOpen (ℂ_{fld})$
		rlimcnp3.k	$⊢ K = J ↾_{𝑡} [0, +∞)$
	Assertion	rlimcnp3	$⊢ φ \to ((y \in ℝ^{+} ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow (x \in [0, +∞) ⟼ if (x = 0, C, R)) \in (K CnP J) (0))$

Proof

Step	Hyp	Ref	Expression
1		rlimcnp3.c	$⊢ φ \to C \in ℂ$
2		rlimcnp3.r	$⊢ (φ \land y \in ℝ^{+}) \to S \in ℂ$
3		rlimcnp3.s	$⊢ y = \frac{1}{x} \to S = R$
4		rlimcnp3.j	$⊢ J = TopOpen (ℂ_{fld})$
5		rlimcnp3.k	$⊢ K = J ↾_{𝑡} [0, +∞)$
6		ssidd	$⊢ φ \to [0, +∞) \subseteq [0, +∞)$
7		0e0icopnf	$⊢ 0 \in [0, +∞)$
8	7	a1i	$⊢ φ \to 0 \in [0, +∞)$
9		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
10	9	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
11		simpr	$⊢ (φ \land y \in ℝ^{+}) \to y \in ℝ^{+}$
12		rpreccl	$⊢ y \in ℝ^{+} \to \frac{1}{y} \in ℝ^{+}$
13	12	adantl	$⊢ (φ \land y \in ℝ^{+}) \to \frac{1}{y} \in ℝ^{+}$
14	13	rpred	$⊢ (φ \land y \in ℝ^{+}) \to \frac{1}{y} \in ℝ$
15	13	rpge0d	$⊢ (φ \land y \in ℝ^{+}) \to 0 \leq \frac{1}{y}$
16		elrege0	$⊢ \frac{1}{y} \in [0, +∞) \leftrightarrow (\frac{1}{y} \in ℝ \land 0 \leq \frac{1}{y})$
17	14 15 16	sylanbrc	$⊢ (φ \land y \in ℝ^{+}) \to \frac{1}{y} \in [0, +∞)$
18	11 17	2thd	$⊢ (φ \land y \in ℝ^{+}) \to (y \in ℝ^{+} \leftrightarrow \frac{1}{y} \in [0, +∞))$
19	6 8 10 1 2 18 3 4 5	rlimcnp2	$⊢ φ \to ((y \in ℝ^{+} ⟼ S) \underset{ℝ}{⇝} C \leftrightarrow (x \in [0, +∞) ⟼ if (x = 0, C, R)) \in (K CnP J) (0))$