Theorem lmclimf

Description: Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 24-Jul-2007) (Revised by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	lmclim.2	|- J = ( TopOpen ` CCfld )
	lmclim.3	|- Z = ( ZZ>= ` M )
Assertion	lmclimf	|- ( ( M e. ZZ /\ F : Z --> CC ) -> ( F ( ~~>t ` J ) P <-> F ~~> P ) )

Proof

Step	Hyp	Ref	Expression
1		lmclim.2	|- J = ( TopOpen ` CCfld )
2		lmclim.3	|- Z = ( ZZ>= ` M )
3		simpr	|- ( ( M e. ZZ /\ F : Z --> CC ) -> F : Z --> CC )
4		uzssz	|- ( ZZ>= ` M ) C_ ZZ
5		zsscn	|- ZZ C_ CC
6	4 5	sstri	|- ( ZZ>= ` M ) C_ CC
7	2 6	eqsstri	|- Z C_ CC
8		cnex	|- CC e. _V
9		elpm2r	|- ( ( ( CC e. _V /\ CC e. _V ) /\ ( F : Z --> CC /\ Z C_ CC ) ) -> F e. ( CC ^pm CC ) )
10	8 8 9	mpanl12	|- ( ( F : Z --> CC /\ Z C_ CC ) -> F e. ( CC ^pm CC ) )
11	3 7 10	sylancl	|- ( ( M e. ZZ /\ F : Z --> CC ) -> F e. ( CC ^pm CC ) )
12		fdm	|- ( F : Z --> CC -> dom F = Z )
13		eqimss2	|- ( dom F = Z -> Z C_ dom F )
14	3 12 13	3syl	|- ( ( M e. ZZ /\ F : Z --> CC ) -> Z C_ dom F )
15	1 2	lmclim	|- ( ( M e. ZZ /\ Z C_ dom F ) -> ( F ( ~~>t ` J ) P <-> ( F e. ( CC ^pm CC ) /\ F ~~> P ) ) )
16	14 15	syldan	|- ( ( M e. ZZ /\ F : Z --> CC ) -> ( F ( ~~>t ` J ) P <-> ( F e. ( CC ^pm CC ) /\ F ~~> P ) ) )
17	11 16	mpbirand	|- ( ( M e. ZZ /\ F : Z --> CC ) -> ( F ( ~~>t ` J ) P <-> F ~~> P ) )