Metamath Proof Explorer

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 ℤ\right)\to {F}\left({k}\right)={F}\left({k}\right)$
4 2 3 clim ${⊢}{F}⇝{A}\to \left({F}⇝{A}↔\left({A}\in ℂ\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\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 {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\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 ℂ$