This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )