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 -> A e. CC )

Proof

Step	Hyp	Ref	Expression
1		climrel	|- Rel ~~>
2	1	brrelex1i	|- ( F ~~> A -> F e. _V )
3		eqidd	|- ( ( F ~~> A /\ k e. ZZ ) -> ( F ` k ) = ( F ` k ) )
4	2 3	clim	|- ( F ~~> A -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) ) )
5	4	ibi	|- ( F ~~> A -> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) ) )
6	5	simpld	|- ( F ~~> A -> A e. CC )