Metamath Proof Explorer

Theorem climisp

Description: If a sequence converges to an isolated point (w.r.t. the standard topology on the complex numbers) then the sequence eventually becomes that point. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses climisp.m 
|- ( ph -> M e. ZZ )
climisp.z 
|- Z = ( ZZ>= ` M )
climisp.f 
|- ( ph -> F : Z --> CC )
climisp.c 
|- ( ph -> F ~~> A )
climisp.x 
|- ( ph -> X e. RR+ )
climisp.l 
|- ( ( ph /\ k e. Z /\ ( F ` k ) =/= A ) -> X <_ ( abs ` ( ( F ` k ) - A ) ) )
Assertion climisp 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) = A )

Proof

Step Hyp Ref Expression
1 climisp.m 
 |-  ( ph -> M e. ZZ )
2 climisp.z 
 |-  Z = ( ZZ>= ` M )
3 climisp.f 
 |-  ( ph -> F : Z --> CC )
4 climisp.c 
 |-  ( ph -> F ~~> A )
5 climisp.x 
 |-  ( ph -> X e. RR+ )
6 climisp.l 
 |-  ( ( ph /\ k e. Z /\ ( F ` k ) =/= A ) -> X <_ ( abs ` ( ( F ` k ) - A ) ) )
7 nfv 
 |-  F/ k ( ph /\ j e. Z )
8 nfra1 
 |-  F/ k A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X )
9 7 8 nfan 
 |-  F/ k ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) )
10 simplll 
 |-  ( ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ph )
11 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
12 11 ad4ant24 
 |-  ( ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
13 rspa 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) )
14 13 simprd 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( F ` k ) - A ) ) < X )
15 14 adantll 
 |-  ( ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( abs ` ( ( F ` k ) - A ) ) < X )
16 simpl3 
 |-  ( ( ( ph /\ k e. Z /\ ( abs ` ( ( F ` k ) - A ) ) < X ) /\ -. ( F ` k ) = A ) -> ( abs ` ( ( F ` k ) - A ) ) < X )
17 neqne 
 |-  ( -. ( F ` k ) = A -> ( F ` k ) =/= A )
18 5 rpred 
 |-  ( ph -> X e. RR )
19 18 ad2antrr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( F ` k ) =/= A ) -> X e. RR )
20 3 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
21 2 fvexi 
 |-  Z e. _V
22 21 a1i 
 |-  ( ph -> Z e. _V )
23 3 22 fexd 
 |-  ( ph -> F e. _V )
24 eqidd 
 |-  ( ( ph /\ k e. ZZ ) -> ( F ` k ) = ( F ` k ) )
25 23 24 clim 
 |-  ( ph -> ( 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 ) ) ) )
26 4 25 mpbid 
 |-  ( ph -> ( 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 ) ) )
27 26 simpld 
 |-  ( ph -> A e. CC )
28 27 adantr 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
29 20 28 subcld 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) - A ) e. CC )
30 29 abscld 
 |-  ( ( ph /\ k e. Z ) -> ( abs ` ( ( F ` k ) - A ) ) e. RR )
31 30 adantr 
 |-  ( ( ( ph /\ k e. Z ) /\ ( F ` k ) =/= A ) -> ( abs ` ( ( F ` k ) - A ) ) e. RR )
32 6 3expa 
 |-  ( ( ( ph /\ k e. Z ) /\ ( F ` k ) =/= A ) -> X <_ ( abs ` ( ( F ` k ) - A ) ) )
33 19 31 32 lensymd 
 |-  ( ( ( ph /\ k e. Z ) /\ ( F ` k ) =/= A ) -> -. ( abs ` ( ( F ` k ) - A ) ) < X )
34 17 33 sylan2 
 |-  ( ( ( ph /\ k e. Z ) /\ -. ( F ` k ) = A ) -> -. ( abs ` ( ( F ` k ) - A ) ) < X )
35 34 3adantl3 
 |-  ( ( ( ph /\ k e. Z /\ ( abs ` ( ( F ` k ) - A ) ) < X ) /\ -. ( F ` k ) = A ) -> -. ( abs ` ( ( F ` k ) - A ) ) < X )
36 16 35 condan 
 |-  ( ( ph /\ k e. Z /\ ( abs ` ( ( F ` k ) - A ) ) < X ) -> ( F ` k ) = A )
37 10 12 15 36 syl3anc 
 |-  ( ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) = A )
38 9 37 ralrimia 
 |-  ( ( ( ph /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) = A )
39 breq2 
 |-  ( x = X -> ( ( abs ` ( ( F ` k ) - A ) ) < x <-> ( abs ` ( ( F ` k ) - A ) ) < X ) )
40 39 anbi2d 
 |-  ( x = X -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) ) )
41 40 rexralbidv 
 |-  ( x = X -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) ) )
42 26 simprd 
 |-  ( ph -> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
43 41 42 5 rspcdva 
 |-  ( ph -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) )
44 2 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) ) )
45 1 44 syl 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) ) )
46 43 45 mpbird 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < X ) )
47 38 46 reximddv3 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) = A )