Metamath Proof Explorer

Theorem lmclim

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

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

Proof

Step Hyp Ref Expression
1 lmclim.2 
 |-  J = ( TopOpen ` CCfld )
2 lmclim.3 
 |-  Z = ( ZZ>= ` M )
3 3anass 
 |-  ( ( F e. ( CC ^pm CC ) /\ P e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) ) <-> ( F e. ( CC ^pm CC ) /\ ( P e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) ) ) )
4 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
5 3anass 
 |-  ( ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) <-> ( k e. dom F /\ ( ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) ) )
6 simplr 
 |-  ( ( ( M e. ZZ /\ Z C_ dom F ) /\ P e. CC ) -> Z C_ dom F )
7 6 sselda 
 |-  ( ( ( ( M e. ZZ /\ Z C_ dom F ) /\ P e. CC ) /\ k e. Z ) -> k e. dom F )
8 7 biantrurd 
 |-  ( ( ( ( M e. ZZ /\ Z C_ dom F ) /\ P e. CC ) /\ k e. Z ) -> ( ( ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) <-> ( k e. dom F /\ ( ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) ) ) )
9 eqid 
 |-  ( abs o. - ) = ( abs o. - )
10 9 cnmetdval 
 |-  ( ( ( F ` k ) e. CC /\ P e. CC ) -> ( ( F ` k ) ( abs o. - ) P ) = ( abs ` ( ( F ` k ) - P ) ) )
11 10 ancoms 
 |-  ( ( P e. CC /\ ( F ` k ) e. CC ) -> ( ( F ` k ) ( abs o. - ) P ) = ( abs ` ( ( F ` k ) - P ) ) )
12 11 breq1d 
 |-  ( ( P e. CC /\ ( F ` k ) e. CC ) -> ( ( ( F ` k ) ( abs o. - ) P ) < x <-> ( abs ` ( ( F ` k ) - P ) ) < x ) )
13 12 pm5.32da 
 |-  ( P e. CC -> ( ( ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) )
14 13 ad2antlr 
 |-  ( ( ( ( M e. ZZ /\ Z C_ dom F ) /\ P e. CC ) /\ k e. Z ) -> ( ( ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) )
15 8 14 bitr3d 
 |-  ( ( ( ( M e. ZZ /\ Z C_ dom F ) /\ P e. CC ) /\ k e. Z ) -> ( ( k e. dom F /\ ( ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) )
16 5 15 syl5bb 
 |-  ( ( ( ( M e. ZZ /\ Z C_ dom F ) /\ P e. CC ) /\ k e. Z ) -> ( ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) )
17 4 16 sylan2 
 |-  ( ( ( ( M e. ZZ /\ Z C_ dom F ) /\ P e. CC ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) )
18 17 anassrs 
 |-  ( ( ( ( ( M e. ZZ /\ Z C_ dom F ) /\ P e. CC ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) )
19 18 ralbidva 
 |-  ( ( ( ( M e. ZZ /\ Z C_ dom F ) /\ P e. CC ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) <-> A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) )
20 19 rexbidva 
 |-  ( ( ( M e. ZZ /\ Z C_ dom F ) /\ P e. CC ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) )
21 20 ralbidv 
 |-  ( ( ( M e. ZZ /\ Z C_ dom F ) /\ P e. CC ) -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) )
22 21 pm5.32da 
 |-  ( ( M e. ZZ /\ Z C_ dom F ) -> ( ( P e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) ) <-> ( P e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) ) )
23 22 anbi2d 
 |-  ( ( M e. ZZ /\ Z C_ dom F ) -> ( ( F e. ( CC ^pm CC ) /\ ( P e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) ) ) <-> ( F e. ( CC ^pm CC ) /\ ( P e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) ) ) )
24 3 23 syl5bb 
 |-  ( ( M e. ZZ /\ Z C_ dom F ) -> ( ( F e. ( CC ^pm CC ) /\ P e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) ) <-> ( F e. ( CC ^pm CC ) /\ ( P e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) ) ) )
25 1 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
26 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
27 26 a1i 
 |-  ( ( M e. ZZ /\ Z C_ dom F ) -> ( abs o. - ) e. ( *Met ` CC ) )
28 simpl 
 |-  ( ( M e. ZZ /\ Z C_ dom F ) -> M e. ZZ )
29 25 27 2 28 lmmbr3 
 |-  ( ( M e. ZZ /\ Z C_ dom F ) -> ( F ( ~~>t ` J ) P <-> ( F e. ( CC ^pm CC ) /\ P e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. CC /\ ( ( F ` k ) ( abs o. - ) P ) < x ) ) ) )
30 simpll 
 |-  ( ( ( M e. ZZ /\ Z C_ dom F ) /\ F e. ( CC ^pm CC ) ) -> M e. ZZ )
31 simpr 
 |-  ( ( ( M e. ZZ /\ Z C_ dom F ) /\ F e. ( CC ^pm CC ) ) -> F e. ( CC ^pm CC ) )
32 eqidd 
 |-  ( ( ( ( M e. ZZ /\ Z C_ dom F ) /\ F e. ( CC ^pm CC ) ) /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
33 2 30 31 32 clim2 
 |-  ( ( ( M e. ZZ /\ Z C_ dom F ) /\ F e. ( CC ^pm CC ) ) -> ( F ~~> P <-> ( P e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) ) )
34 33 pm5.32da 
 |-  ( ( M e. ZZ /\ Z C_ dom F ) -> ( ( F e. ( CC ^pm CC ) /\ F ~~> P ) <-> ( F e. ( CC ^pm CC ) /\ ( P e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - P ) ) < x ) ) ) ) )
35 24 29 34 3bitr4d 
 |-  ( ( M e. ZZ /\ Z C_ dom F ) -> ( F ( ~~>t ` J ) P <-> ( F e. ( CC ^pm CC ) /\ F ~~> P ) ) )