Metamath Proof Explorer

Theorem climrescn

Description: A sequence converging w.r.t. the standard topology on the complex numbers, eventually becomes a sequence of complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses climrescn.m 
|- ( ph -> M e. ZZ )
climrescn.z 
|- Z = ( ZZ>= ` M )
climrescn.f 
|- ( ph -> F Fn Z )
climrescn.c 
|- ( ph -> F e. dom ~~> )
Assertion climrescn 
|- ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC )

Proof

Step Hyp Ref Expression
1 climrescn.m 
 |-  ( ph -> M e. ZZ )
2 climrescn.z 
 |-  Z = ( ZZ>= ` M )
3 climrescn.f 
 |-  ( ph -> F Fn Z )
4 climrescn.c 
 |-  ( ph -> F e. dom ~~> )
5 nfv 
 |-  F/ k ( ph /\ i e. Z )
6 nfra1 
 |-  F/ k A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 )
7 5 6 nfan 
 |-  F/ k ( ( ph /\ i e. Z ) /\ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) )
8 2 uztrn2 
 |-  ( ( i e. Z /\ k e. ( ZZ>= ` i ) ) -> k e. Z )
9 8 adantll 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> k e. Z )
10 3 fndmd 
 |-  ( ph -> dom F = Z )
11 10 ad2antrr 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> dom F = Z )
12 9 11 eleqtrrd 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> k e. dom F )
13 12 adantlr 
 |-  ( ( ( ( ph /\ i e. Z ) /\ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) /\ k e. ( ZZ>= ` i ) ) -> k e. dom F )
14 rspa 
 |-  ( ( A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) /\ k e. ( ZZ>= ` i ) ) -> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) )
15 14 adantll 
 |-  ( ( ( i e. Z /\ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) /\ k e. ( ZZ>= ` i ) ) -> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) )
16 15 simpld 
 |-  ( ( ( i e. Z /\ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) /\ k e. ( ZZ>= ` i ) ) -> ( F ` k ) e. CC )
17 16 adantlll 
 |-  ( ( ( ( ph /\ i e. Z ) /\ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) /\ k e. ( ZZ>= ` i ) ) -> ( F ` k ) e. CC )
18 13 17 jca 
 |-  ( ( ( ( ph /\ i e. Z ) /\ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) /\ k e. ( ZZ>= ` i ) ) -> ( k e. dom F /\ ( F ` k ) e. CC ) )
19 7 18 ralrimia 
 |-  ( ( ( ph /\ i e. Z ) /\ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) -> A. k e. ( ZZ>= ` i ) ( k e. dom F /\ ( F ` k ) e. CC ) )
20 fnfun 
 |-  ( F Fn Z -> Fun F )
21 ffvresb 
 |-  ( Fun F -> ( ( F |` ( ZZ>= ` i ) ) : ( ZZ>= ` i ) --> CC <-> A. k e. ( ZZ>= ` i ) ( k e. dom F /\ ( F ` k ) e. CC ) ) )
22 3 20 21 3syl 
 |-  ( ph -> ( ( F |` ( ZZ>= ` i ) ) : ( ZZ>= ` i ) --> CC <-> A. k e. ( ZZ>= ` i ) ( k e. dom F /\ ( F ` k ) e. CC ) ) )
23 22 ad2antrr 
 |-  ( ( ( ph /\ i e. Z ) /\ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) -> ( ( F |` ( ZZ>= ` i ) ) : ( ZZ>= ` i ) --> CC <-> A. k e. ( ZZ>= ` i ) ( k e. dom F /\ ( F ` k ) e. CC ) ) )
24 19 23 mpbird 
 |-  ( ( ( ph /\ i e. Z ) /\ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) -> ( F |` ( ZZ>= ` i ) ) : ( ZZ>= ` i ) --> CC )
25 breq2 
 |-  ( x = 1 -> ( ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < x <-> ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) )
26 25 anbi2d 
 |-  ( x = 1 -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) )
27 26 rexralbidv 
 |-  ( x = 1 -> ( E. i e. ZZ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < x ) <-> E. i e. ZZ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) )
28 climdm 
 |-  ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) )
29 4 28 sylib 
 |-  ( ph -> F ~~> ( ~~> ` F ) )
30 eqidd 
 |-  ( ( ph /\ k e. ZZ ) -> ( F ` k ) = ( F ` k ) )
31 4 30 clim 
 |-  ( ph -> ( F ~~> ( ~~> ` F ) <-> ( ( ~~> ` F ) e. CC /\ A. x e. RR+ E. i e. ZZ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < x ) ) ) )
32 29 31 mpbid 
 |-  ( ph -> ( ( ~~> ` F ) e. CC /\ A. x e. RR+ E. i e. ZZ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < x ) ) )
33 32 simprd 
 |-  ( ph -> A. x e. RR+ E. i e. ZZ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < x ) )
34 1rp 
 |-  1 e. RR+
35 34 a1i 
 |-  ( ph -> 1 e. RR+ )
36 27 33 35 rspcdva 
 |-  ( ph -> E. i e. ZZ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) )
37 2 rexuz3 
 |-  ( M e. ZZ -> ( E. i e. Z A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) <-> E. i e. ZZ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) )
38 1 37 syl 
 |-  ( ph -> ( E. i e. Z A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) <-> E. i e. ZZ A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) ) )
39 36 38 mpbird 
 |-  ( ph -> E. i e. Z A. k e. ( ZZ>= ` i ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( ~~> ` F ) ) ) < 1 ) )
40 24 39 reximddv3 
 |-  ( ph -> E. i e. Z ( F |` ( ZZ>= ` i ) ) : ( ZZ>= ` i ) --> CC )
41 fveq2 
 |-  ( j = i -> ( ZZ>= ` j ) = ( ZZ>= ` i ) )
42 41 reseq2d 
 |-  ( j = i -> ( F |` ( ZZ>= ` j ) ) = ( F |` ( ZZ>= ` i ) ) )
43 42 41 feq12d 
 |-  ( j = i -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC <-> ( F |` ( ZZ>= ` i ) ) : ( ZZ>= ` i ) --> CC ) )
44 43 cbvrexvw 
 |-  ( E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC <-> E. i e. Z ( F |` ( ZZ>= ` i ) ) : ( ZZ>= ` i ) --> CC )
45 40 44 sylibr 
 |-  ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> CC )