Metamath Proof Explorer

Theorem xlimxrre

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 xlimxrre.m 
|- ( ph -> M e. ZZ )
xlimxrre.z 
|- Z = ( ZZ>= ` M )
xlimxrre.f 
|- ( ph -> F : Z --> RR* )
xlimxrre.a 
|- ( ph -> A e. RR )
xlimxrre.c 
|- ( ph -> F ~~>* A )
Assertion xlimxrre 
|- ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )

Proof

Step Hyp Ref Expression
1 xlimxrre.m 
 |-  ( ph -> M e. ZZ )
2 xlimxrre.z 
 |-  Z = ( ZZ>= ` M )
3 xlimxrre.f 
 |-  ( ph -> F : Z --> RR* )
4 xlimxrre.a 
 |-  ( ph -> A e. RR )
5 xlimxrre.c 
 |-  ( ph -> F ~~>* A )
6 elioore 
 |-  ( ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) -> ( F ` k ) e. RR )
7 6 anim2i 
 |-  ( ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) -> ( k e. dom F /\ ( F ` k ) e. RR ) )
8 7 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) )
9 8 adantl 
 |-  ( ( ph /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) ) -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) )
10 3 ffund 
 |-  ( ph -> Fun F )
11 ffvresb 
 |-  ( Fun F -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) ) )
12 10 11 syl 
 |-  ( ph -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) ) )
13 12 adantr 
 |-  ( ( ph /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) ) -> ( ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. RR ) ) )
14 9 13 mpbird 
 |-  ( ( ph /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) ) -> ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
15 14 adantrl 
 |-  ( ( ph /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) ) ) -> ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )
16 peano2rem 
 |-  ( A e. RR -> ( A - 1 ) e. RR )
17 4 16 syl 
 |-  ( ph -> ( A - 1 ) e. RR )
18 17 rexrd 
 |-  ( ph -> ( A - 1 ) e. RR* )
19 peano2re 
 |-  ( A e. RR -> ( A + 1 ) e. RR )
20 4 19 syl 
 |-  ( ph -> ( A + 1 ) e. RR )
21 20 rexrd 
 |-  ( ph -> ( A + 1 ) e. RR* )
22 4 ltm1d 
 |-  ( ph -> ( A - 1 ) < A )
23 4 ltp1d 
 |-  ( ph -> A < ( A + 1 ) )
24 18 21 4 22 23 eliood 
 |-  ( ph -> A e. ( ( A - 1 ) (,) ( A + 1 ) ) )
25 iooordt 
 |-  ( ( A - 1 ) (,) ( A + 1 ) ) e. ( ordTop ` <_ )
26 nfcv 
 |-  F/_ k F
27 eqid 
 |-  ( ordTop ` <_ ) = ( ordTop ` <_ )
28 26 1 2 3 27 xlimbr 
 |-  ( ph -> ( F ~~>* A <-> ( A e. RR* /\ A. u e. ( ordTop ` <_ ) ( A e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
29 5 28 mpbid 
 |-  ( ph -> ( A e. RR* /\ A. u e. ( ordTop ` <_ ) ( A e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
30 29 simprd 
 |-  ( ph -> A. u e. ( ordTop ` <_ ) ( A e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
31 eleq2 
 |-  ( u = ( ( A - 1 ) (,) ( A + 1 ) ) -> ( A e. u <-> A e. ( ( A - 1 ) (,) ( A + 1 ) ) ) )
32 eleq2 
 |-  ( u = ( ( A - 1 ) (,) ( A + 1 ) ) -> ( ( F ` k ) e. u <-> ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) )
33 32 anbi2d 
 |-  ( u = ( ( A - 1 ) (,) ( A + 1 ) ) -> ( ( k e. dom F /\ ( F ` k ) e. u ) <-> ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) ) )
34 33 rexralbidv 
 |-  ( u = ( ( A - 1 ) (,) ( A + 1 ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) ) )
35 31 34 imbi12d 
 |-  ( u = ( ( A - 1 ) (,) ( A + 1 ) ) -> ( ( A e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) <-> ( A e. ( ( A - 1 ) (,) ( A + 1 ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) ) ) )
36 35 rspcva 
 |-  ( ( ( ( A - 1 ) (,) ( A + 1 ) ) e. ( ordTop ` <_ ) /\ A. u e. ( ordTop ` <_ ) ( A e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) -> ( A e. ( ( A - 1 ) (,) ( A + 1 ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) ) )
37 25 30 36 sylancr 
 |-  ( ph -> ( A e. ( ( A - 1 ) (,) ( A + 1 ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) ) )
38 24 37 mpd 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( ( A - 1 ) (,) ( A + 1 ) ) ) )
39 15 38 reximddv 
 |-  ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> RR )