This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimcl

Description: Closure of the limit of a sequence of complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	rlimcl	$⊢ F \underset{ℝ}{⇝} A \to A \in ℂ$

Proof

Step	Hyp	Ref	Expression
1		rlimf	$⊢ F \underset{ℝ}{⇝} A \to F : dom F ⟶ ℂ$
2		rlimss	$⊢ F \underset{ℝ}{⇝} A \to dom F \subseteq ℝ$
3		eqidd	$⊢ (F \underset{ℝ}{⇝} A \land x \in dom F) \to F (x) = F (x)$
4	1 2 3	rlim	$⊢ F \underset{ℝ}{⇝} A \to (F \underset{ℝ}{⇝} A \leftrightarrow (A \in ℂ \land \forall y \in ℝ^{+} \exists z \in ℝ \forall x \in dom F (z \leq x \to \|F (x) - A\| < y)))$
5	4	ibi	$⊢ F \underset{ℝ}{⇝} A \to (A \in ℂ \land \forall y \in ℝ^{+} \exists z \in ℝ \forall x \in dom F (z \leq x \to \|F (x) - A\| < y))$
6	5	simpld	$⊢ F \underset{ℝ}{⇝} A \to A \in ℂ$