Metamath Proof Explorer

Theorem climxrrelem

Description: If a seqence ranging over the extended reals converges w.r.t. the standard topology on the complex numbers, then there exists an upper set of the integers over which the function is real-valued. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses climxrrelem.m 
|- ( ph -> M e. ZZ )
climxrrelem.z 
|- Z = ( ZZ>= ` M )
climxrrelem.f 
|- ( ph -> F : Z --> RR* )
climxrrelem.c 
|- ( ph -> F ~~> A )
climxrrelem.d 
|- ( ph -> D e. RR+ )
climxrrelem.p 
|- ( ( ph /\ +oo e. CC ) -> D <_ ( abs ` ( +oo - A ) ) )
climxrrelem.n 
|- ( ( ph /\ -oo e. CC ) -> D <_ ( abs ` ( -oo - A ) ) )
Assertion climxrrelem 
|- ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )

Proof

Step Hyp Ref Expression
1 climxrrelem.m 
 |-  ( ph -> M e. ZZ )
2 climxrrelem.z 
 |-  Z = ( ZZ>= ` M )
3 climxrrelem.f 
 |-  ( ph -> F : Z --> RR* )
4 climxrrelem.c 
 |-  ( ph -> F ~~> A )
5 climxrrelem.d 
 |-  ( ph -> D e. RR+ )
6 climxrrelem.p 
 |-  ( ( ph /\ +oo e. CC ) -> D <_ ( abs ` ( +oo - A ) ) )
7 climxrrelem.n 
 |-  ( ( ph /\ -oo e. CC ) -> D <_ ( abs ` ( -oo - A ) ) )
8 nfv 
 |-  F/ k ph
9 nfv 
 |-  F/ k j e. Z
10 nfra1 
 |-  F/ k A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D )
11 9 10 nfan 
 |-  F/ k ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) )
12 8 11 nfan 
 |-  F/ k ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) )
13 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
14 13 adantll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
15 3 fdmd 
 |-  ( ph -> dom F = Z )
16 15 ad2antrr 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> dom F = Z )
17 14 16 eleqtrrd 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> k e. dom F )
18 17 adantlrr 
 |-  ( ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. dom F )
19 simpll 
 |-  ( ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ph )
20 14 adantlrr 
 |-  ( ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
21 rspa 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) )
22 21 adantll 
 |-  ( ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) )
23 22 adantll 
 |-  ( ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) )
24 3 ffvelrnda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR* )
25 24 3adant3 
 |-  ( ( ph /\ k e. Z /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) -> ( F ` k ) e. RR* )
26 simpll 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = -oo ) -> ph )
27 simpr 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` k ) = -oo ) -> ( F ` k ) = -oo )
28 simpl 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` k ) = -oo ) -> ( F ` k ) e. CC )
29 27 28 eqeltrrd 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` k ) = -oo ) -> -oo e. CC )
30 29 adantll 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = -oo ) -> -oo e. CC )
31 26 30 7 syl2anc 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = -oo ) -> D <_ ( abs ` ( -oo - A ) ) )
32 31 adantlrr 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = -oo ) -> D <_ ( abs ` ( -oo - A ) ) )
33 fvoveq1 
 |-  ( ( F ` k ) = -oo -> ( abs ` ( ( F ` k ) - A ) ) = ( abs ` ( -oo - A ) ) )
34 33 adantl 
 |-  ( ( ( abs ` ( ( F ` k ) - A ) ) < D /\ ( F ` k ) = -oo ) -> ( abs ` ( ( F ` k ) - A ) ) = ( abs ` ( -oo - A ) ) )
35 simpl 
 |-  ( ( ( abs ` ( ( F ` k ) - A ) ) < D /\ ( F ` k ) = -oo ) -> ( abs ` ( ( F ` k ) - A ) ) < D )
36 34 35 eqbrtrrd 
 |-  ( ( ( abs ` ( ( F ` k ) - A ) ) < D /\ ( F ` k ) = -oo ) -> ( abs ` ( -oo - A ) ) < D )
37 36 adantll 
 |-  ( ( ( ph /\ ( abs ` ( ( F ` k ) - A ) ) < D ) /\ ( F ` k ) = -oo ) -> ( abs ` ( -oo - A ) ) < D )
38 37 adantlrl 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = -oo ) -> ( abs ` ( -oo - A ) ) < D )
39 2 fvexi 
 |-  Z e. _V
40 39 a1i 
 |-  ( ph -> Z e. _V )
41 3 40 fexd 
 |-  ( ph -> F e. _V )
42 eqidd 
 |-  ( ( ph /\ k e. ZZ ) -> ( F ` k ) = ( F ` k ) )
43 41 42 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 ) ) ) )
44 4 43 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 ) ) )
45 44 simpld 
 |-  ( ph -> A e. CC )
46 45 ad2antrr 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = -oo ) -> A e. CC )
47 30 46 subcld 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = -oo ) -> ( -oo - A ) e. CC )
48 47 abscld 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = -oo ) -> ( abs ` ( -oo - A ) ) e. RR )
49 48 adantlrr 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = -oo ) -> ( abs ` ( -oo - A ) ) e. RR )
50 5 rpred 
 |-  ( ph -> D e. RR )
51 50 ad2antrr 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = -oo ) -> D e. RR )
52 49 51 ltnled 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = -oo ) -> ( ( abs ` ( -oo - A ) ) < D <-> -. D <_ ( abs ` ( -oo - A ) ) ) )
53 38 52 mpbid 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = -oo ) -> -. D <_ ( abs ` ( -oo - A ) ) )
54 32 53 pm2.65da 
 |-  ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) -> -. ( F ` k ) = -oo )
55 54 3adant2 
 |-  ( ( ph /\ k e. Z /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) -> -. ( F ` k ) = -oo )
56 55 neqned 
 |-  ( ( ph /\ k e. Z /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) -> ( F ` k ) =/= -oo )
57 simpll 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = +oo ) -> ph )
58 simpr 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` k ) = +oo ) -> ( F ` k ) = +oo )
59 simpl 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` k ) = +oo ) -> ( F ` k ) e. CC )
60 58 59 eqeltrrd 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` k ) = +oo ) -> +oo e. CC )
61 60 adantll 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = +oo ) -> +oo e. CC )
62 57 61 6 syl2anc 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = +oo ) -> D <_ ( abs ` ( +oo - A ) ) )
63 62 adantlrr 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = +oo ) -> D <_ ( abs ` ( +oo - A ) ) )
64 fvoveq1 
 |-  ( ( F ` k ) = +oo -> ( abs ` ( ( F ` k ) - A ) ) = ( abs ` ( +oo - A ) ) )
65 64 adantl 
 |-  ( ( ( abs ` ( ( F ` k ) - A ) ) < D /\ ( F ` k ) = +oo ) -> ( abs ` ( ( F ` k ) - A ) ) = ( abs ` ( +oo - A ) ) )
66 simpl 
 |-  ( ( ( abs ` ( ( F ` k ) - A ) ) < D /\ ( F ` k ) = +oo ) -> ( abs ` ( ( F ` k ) - A ) ) < D )
67 65 66 eqbrtrrd 
 |-  ( ( ( abs ` ( ( F ` k ) - A ) ) < D /\ ( F ` k ) = +oo ) -> ( abs ` ( +oo - A ) ) < D )
68 67 adantll 
 |-  ( ( ( ph /\ ( abs ` ( ( F ` k ) - A ) ) < D ) /\ ( F ` k ) = +oo ) -> ( abs ` ( +oo - A ) ) < D )
69 68 adantlrl 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = +oo ) -> ( abs ` ( +oo - A ) ) < D )
70 45 ad2antrr 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = +oo ) -> A e. CC )
71 61 70 subcld 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = +oo ) -> ( +oo - A ) e. CC )
72 71 abscld 
 |-  ( ( ( ph /\ ( F ` k ) e. CC ) /\ ( F ` k ) = +oo ) -> ( abs ` ( +oo - A ) ) e. RR )
73 72 adantlrr 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = +oo ) -> ( abs ` ( +oo - A ) ) e. RR )
74 50 ad2antrr 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = +oo ) -> D e. RR )
75 73 74 ltnled 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = +oo ) -> ( ( abs ` ( +oo - A ) ) < D <-> -. D <_ ( abs ` ( +oo - A ) ) ) )
76 69 75 mpbid 
 |-  ( ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) /\ ( F ` k ) = +oo ) -> -. D <_ ( abs ` ( +oo - A ) ) )
77 63 76 pm2.65da 
 |-  ( ( ph /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) -> -. ( F ` k ) = +oo )
78 77 3adant2 
 |-  ( ( ph /\ k e. Z /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) -> -. ( F ` k ) = +oo )
79 78 neqned 
 |-  ( ( ph /\ k e. Z /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) -> ( F ` k ) =/= +oo )
80 25 56 79 xrred 
 |-  ( ( ph /\ k e. Z /\ ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) -> ( F ` k ) e. RR )
81 19 20 23 80 syl3anc 
 |-  ( ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR )
82 18 81 jca 
 |-  ( ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) ) /\ k e. ( ZZ>= ` j ) ) -> ( k e. dom F /\ ( F ` k ) e. RR ) )
83 12 82 ralrimia 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) ) -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) )
84 3 ffund 
 |-  ( ph -> Fun F )
85 ffvresb 
 |-  ( Fun F -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) ) )
86 84 85 syl 
 |-  ( ph -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) ) )
87 86 adantr 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) ) -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) ) )
88 83 87 mpbird 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) ) -> ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
89 breq2 
 |-  ( x = D -> ( ( abs ` ( ( F ` k ) - A ) ) < x <-> ( abs ` ( ( F ` k ) - A ) ) < D ) )
90 89 anbi2d 
 |-  ( x = D -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) )
91 90 rexralbidv 
 |-  ( x = D -> ( 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 ) ) < D ) ) )
92 44 simprd 
 |-  ( ph -> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
93 91 92 5 rspcdva 
 |-  ( ph -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) )
94 2 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) )
95 1 94 syl 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) ) )
96 93 95 mpbird 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < D ) )
97 88 96 reximddv 
 |-  ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )