Metamath Proof Explorer

Theorem climxrre

Description: If a sequence 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 (the weaker hypothesis F e. dom ~> is probably not enough, since in principle we could have +oo e. CC and -oo e. CC ). (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses climxrre.m 
|- ( ph -> M e. ZZ )
climxrre.z 
|- Z = ( ZZ>= ` M )
climxrre.f 
|- ( ph -> F : Z --> RR* )
climxrre.a 
|- ( ph -> A e. RR )
climxrre.c 
|- ( ph -> F ~~> A )
Assertion climxrre 
|- ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )

Proof

Step Hyp Ref Expression
1 climxrre.m 
 |-  ( ph -> M e. ZZ )
2 climxrre.z 
 |-  Z = ( ZZ>= ` M )
3 climxrre.f 
 |-  ( ph -> F : Z --> RR* )
4 climxrre.a 
 |-  ( ph -> A e. RR )
5 climxrre.c 
 |-  ( ph -> F ~~> A )
6 1 ad2antrr 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) -> M e. ZZ )
7 3 ad2antrr 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) -> F : Z --> RR* )
8 5 ad2antrr 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) -> F ~~> A )
9 simpr 
 |-  ( ( ph /\ +oo e. CC ) -> +oo e. CC )
10 4 recnd 
 |-  ( ph -> A e. CC )
11 10 adantr 
 |-  ( ( ph /\ +oo e. CC ) -> A e. CC )
12 9 11 subcld 
 |-  ( ( ph /\ +oo e. CC ) -> ( +oo - A ) e. CC )
13 renepnf 
 |-  ( A e. RR -> A =/= +oo )
14 13 necomd 
 |-  ( A e. RR -> +oo =/= A )
15 4 14 syl 
 |-  ( ph -> +oo =/= A )
16 15 adantr 
 |-  ( ( ph /\ +oo e. CC ) -> +oo =/= A )
17 9 11 16 subne0d 
 |-  ( ( ph /\ +oo e. CC ) -> ( +oo - A ) =/= 0 )
18 12 17 absrpcld 
 |-  ( ( ph /\ +oo e. CC ) -> ( abs ` ( +oo - A ) ) e. RR+ )
19 18 adantr 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) -> ( abs ` ( +oo - A ) ) e. RR+ )
20 simpr 
 |-  ( ( ph /\ -oo e. CC ) -> -oo e. CC )
21 10 adantr 
 |-  ( ( ph /\ -oo e. CC ) -> A e. CC )
22 20 21 subcld 
 |-  ( ( ph /\ -oo e. CC ) -> ( -oo - A ) e. CC )
23 4 adantr 
 |-  ( ( ph /\ -oo e. CC ) -> A e. RR )
24 renemnf 
 |-  ( A e. RR -> A =/= -oo )
25 24 necomd 
 |-  ( A e. RR -> -oo =/= A )
26 23 25 syl 
 |-  ( ( ph /\ -oo e. CC ) -> -oo =/= A )
27 20 21 26 subne0d 
 |-  ( ( ph /\ -oo e. CC ) -> ( -oo - A ) =/= 0 )
28 22 27 absrpcld 
 |-  ( ( ph /\ -oo e. CC ) -> ( abs ` ( -oo - A ) ) e. RR+ )
29 28 adantlr 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) -> ( abs ` ( -oo - A ) ) e. RR+ )
30 19 29 ifcld 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) -> if ( ( abs ` ( +oo - A ) ) <_ ( abs ` ( -oo - A ) ) , ( abs ` ( +oo - A ) ) , ( abs ` ( -oo - A ) ) ) e. RR+ )
31 19 rpred 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) -> ( abs ` ( +oo - A ) ) e. RR )
32 29 rpred 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) -> ( abs ` ( -oo - A ) ) e. RR )
33 31 32 min1d 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) -> if ( ( abs ` ( +oo - A ) ) <_ ( abs ` ( -oo - A ) ) , ( abs ` ( +oo - A ) ) , ( abs ` ( -oo - A ) ) ) <_ ( abs ` ( +oo - A ) ) )
34 33 adantr 
 |-  ( ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) /\ +oo e. CC ) -> if ( ( abs ` ( +oo - A ) ) <_ ( abs ` ( -oo - A ) ) , ( abs ` ( +oo - A ) ) , ( abs ` ( -oo - A ) ) ) <_ ( abs ` ( +oo - A ) ) )
35 31 32 min2d 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) -> if ( ( abs ` ( +oo - A ) ) <_ ( abs ` ( -oo - A ) ) , ( abs ` ( +oo - A ) ) , ( abs ` ( -oo - A ) ) ) <_ ( abs ` ( -oo - A ) ) )
36 35 adantr 
 |-  ( ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) /\ -oo e. CC ) -> if ( ( abs ` ( +oo - A ) ) <_ ( abs ` ( -oo - A ) ) , ( abs ` ( +oo - A ) ) , ( abs ` ( -oo - A ) ) ) <_ ( abs ` ( -oo - A ) ) )
37 6 2 7 8 30 34 36 climxrrelem 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -oo e. CC ) -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
38 1 ad2antrr 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -. -oo e. CC ) -> M e. ZZ )
39 3 ad2antrr 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -. -oo e. CC ) -> F : Z --> RR* )
40 5 ad2antrr 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -. -oo e. CC ) -> F ~~> A )
41 18 adantr 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -. -oo e. CC ) -> ( abs ` ( +oo - A ) ) e. RR+ )
42 18 rpred 
 |-  ( ( ph /\ +oo e. CC ) -> ( abs ` ( +oo - A ) ) e. RR )
43 42 leidd 
 |-  ( ( ph /\ +oo e. CC ) -> ( abs ` ( +oo - A ) ) <_ ( abs ` ( +oo - A ) ) )
44 43 ad2antrr 
 |-  ( ( ( ( ph /\ +oo e. CC ) /\ -. -oo e. CC ) /\ +oo e. CC ) -> ( abs ` ( +oo - A ) ) <_ ( abs ` ( +oo - A ) ) )
45 pm2.21 
 |-  ( -. -oo e. CC -> ( -oo e. CC -> ( abs ` ( +oo - A ) ) <_ ( abs ` ( -oo - A ) ) ) )
46 45 imp 
 |-  ( ( -. -oo e. CC /\ -oo e. CC ) -> ( abs ` ( +oo - A ) ) <_ ( abs ` ( -oo - A ) ) )
47 46 adantll 
 |-  ( ( ( ( ph /\ +oo e. CC ) /\ -. -oo e. CC ) /\ -oo e. CC ) -> ( abs ` ( +oo - A ) ) <_ ( abs ` ( -oo - A ) ) )
48 38 2 39 40 41 44 47 climxrrelem 
 |-  ( ( ( ph /\ +oo e. CC ) /\ -. -oo e. CC ) -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
49 37 48 pm2.61dan 
 |-  ( ( ph /\ +oo e. CC ) -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
50 1 ad2antrr 
 |-  ( ( ( ph /\ -. +oo e. CC ) /\ -oo e. CC ) -> M e. ZZ )
51 3 ad2antrr 
 |-  ( ( ( ph /\ -. +oo e. CC ) /\ -oo e. CC ) -> F : Z --> RR* )
52 5 ad2antrr 
 |-  ( ( ( ph /\ -. +oo e. CC ) /\ -oo e. CC ) -> F ~~> A )
53 28 adantlr 
 |-  ( ( ( ph /\ -. +oo e. CC ) /\ -oo e. CC ) -> ( abs ` ( -oo - A ) ) e. RR+ )
54 pm2.21 
 |-  ( -. +oo e. CC -> ( +oo e. CC -> ( abs ` ( -oo - A ) ) <_ ( abs ` ( +oo - A ) ) ) )
55 54 imp 
 |-  ( ( -. +oo e. CC /\ +oo e. CC ) -> ( abs ` ( -oo - A ) ) <_ ( abs ` ( +oo - A ) ) )
56 55 ad4ant24 
 |-  ( ( ( ( ph /\ -. +oo e. CC ) /\ -oo e. CC ) /\ +oo e. CC ) -> ( abs ` ( -oo - A ) ) <_ ( abs ` ( +oo - A ) ) )
57 28 rpred 
 |-  ( ( ph /\ -oo e. CC ) -> ( abs ` ( -oo - A ) ) e. RR )
58 57 leidd 
 |-  ( ( ph /\ -oo e. CC ) -> ( abs ` ( -oo - A ) ) <_ ( abs ` ( -oo - A ) ) )
59 58 ad4ant13 
 |-  ( ( ( ( ph /\ -. +oo e. CC ) /\ -oo e. CC ) /\ -oo e. CC ) -> ( abs ` ( -oo - A ) ) <_ ( abs ` ( -oo - A ) ) )
60 50 2 51 52 53 56 59 climxrrelem 
 |-  ( ( ( ph /\ -. +oo e. CC ) /\ -oo e. CC ) -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
61 nfv 
 |-  F/ k ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC )
62 nfv 
 |-  F/ k j e. Z
63 nfra1 
 |-  F/ k A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC
64 62 63 nfan 
 |-  F/ k ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC )
65 61 64 nfan 
 |-  F/ k ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) )
66 simp-4l 
 |-  ( ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) /\ k e. ( ZZ>= ` j ) ) -> ph )
67 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
68 67 adantlr 
 |-  ( ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
69 68 adantll 
 |-  ( ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
70 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
71 3 fdmd 
 |-  ( ph -> dom F = Z )
72 71 adantr 
 |-  ( ( ph /\ k e. Z ) -> dom F = Z )
73 70 72 eleqtrrd 
 |-  ( ( ph /\ k e. Z ) -> k e. dom F )
74 66 69 73 syl2anc 
 |-  ( ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) /\ k e. ( ZZ>= ` j ) ) -> k e. dom F )
75 3 ffvelrnda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR* )
76 66 69 75 syl2anc 
 |-  ( ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR* )
77 rspa 
 |-  ( ( A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. CC )
78 77 adantll 
 |-  ( ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. CC )
79 78 adantll 
 |-  ( ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. CC )
80 simpllr 
 |-  ( ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) /\ k e. ( ZZ>= ` j ) ) -> -. -oo e. CC )
81 nelne2 
 |-  ( ( ( F ` k ) e. CC /\ -. -oo e. CC ) -> ( F ` k ) =/= -oo )
82 79 80 81 syl2anc 
 |-  ( ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) =/= -oo )
83 simp-4r 
 |-  ( ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) /\ k e. ( ZZ>= ` j ) ) -> -. +oo e. CC )
84 nelne2 
 |-  ( ( ( F ` k ) e. CC /\ -. +oo e. CC ) -> ( F ` k ) =/= +oo )
85 79 83 84 syl2anc 
 |-  ( ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) =/= +oo )
86 76 82 85 xrred 
 |-  ( ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR )
87 74 86 jca 
 |-  ( ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) /\ k e. ( ZZ>= ` j ) ) -> ( k e. dom F /\ ( F ` k ) e. RR ) )
88 65 87 ralrimia 
 |-  ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) )
89 3 ffund 
 |-  ( ph -> Fun F )
90 ffvresb 
 |-  ( Fun F -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) ) )
91 89 90 syl 
 |-  ( ph -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) ) )
92 91 ad3antrrr 
 |-  ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) ) )
93 88 92 mpbird 
 |-  ( ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) ) -> ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
94 r19.26 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < 1 ) <-> ( A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC /\ A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - A ) ) < 1 ) )
95 94 simplbi 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < 1 ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC )
96 95 ad2antll 
 |-  ( ( ph /\ ( j e. ZZ /\ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < 1 ) ) ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC )
97 breq2 
 |-  ( x = 1 -> ( ( abs ` ( ( F ` k ) - A ) ) < x <-> ( abs ` ( ( F ` k ) - A ) ) < 1 ) )
98 97 anbi2d 
 |-  ( x = 1 -> ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) <-> ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < 1 ) ) )
99 98 rexralbidv 
 |-  ( x = 1 -> ( 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 ) ) < 1 ) ) )
100 2 fvexi 
 |-  Z e. _V
101 100 a1i 
 |-  ( ph -> Z e. _V )
102 3 101 fexd 
 |-  ( ph -> F e. _V )
103 eqidd 
 |-  ( ( ph /\ k e. ZZ ) -> ( F ` k ) = ( F ` k ) )
104 102 103 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 ) ) ) )
105 5 104 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 ) ) )
106 105 simprd 
 |-  ( ph -> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < x ) )
107 1rp 
 |-  1 e. RR+
108 107 a1i 
 |-  ( ph -> 1 e. RR+ )
109 99 106 108 rspcdva 
 |-  ( ph -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - A ) ) < 1 ) )
110 96 109 reximddv 
 |-  ( ph -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC )
111 2 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) )
112 1 111 syl 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC ) )
113 110 112 mpbird 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC )
114 113 ad2antrr 
 |-  ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC )
115 93 114 reximddv 
 |-  ( ( ( ph /\ -. +oo e. CC ) /\ -. -oo e. CC ) -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
116 60 115 pm2.61dan 
 |-  ( ( ph /\ -. +oo e. CC ) -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
117 49 116 pm2.61dan 
 |-  ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )