climcl

Description: Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	climcl	$⊢ F ⇝ A \to A \in ℂ$

Step	Hyp	Ref	Expression
1		climrel	$⊢ Rel ⇝$
2	1	brrelex1i	$⊢ F ⇝ A \to F \in V$
3		eqidd	$⊢ (F ⇝ A \land k \in ℤ) \to F (k) = F (k)$
4	2 3	clim	$⊢ F ⇝ A \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)))$
5	4	ibi	$⊢ F ⇝ A \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
6	5	simpld	$⊢ F ⇝ A \to A \in ℂ$

Metamath Proof Explorer