Theorem 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 ℂ$$

Proof

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