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:\mathrm{dom}F⟶ℂ$$
2		rlimss	$$⊢F\underset{ℝ}{⇝}A\to \mathrm{dom}F\subseteq ℝ$$
3		eqidd	$$⊢\left(F\underset{ℝ}{⇝}A\wedge x\in \mathrm{dom}F\right)\to F\left(x\right)=F\left(x\right)$$
4	1 2 3	rlim	$$⊢F\underset{ℝ}{⇝}A\to \left(F\underset{ℝ}{⇝}A\leftrightarrow \left(A\in ℂ\wedge \forall y\in {ℝ}^{+}\exists z\in ℝ\forall x\in \mathrm{dom}F\left(z\le x\to \left|F\left(x\right)-A\right|<y\right)\right)\right)$$
5	4	ibi	$$⊢F\underset{ℝ}{⇝}A\to \left(A\in ℂ\wedge \forall y\in {ℝ}^{+}\exists z\in ℝ\forall x\in \mathrm{dom}F\left(z\le x\to \left|F\left(x\right)-A\right|<y\right)\right)$$
6	5	simpld	$$⊢F\underset{ℝ}{⇝}A\to A\in ℂ$$