Metamath Proof Explorer

Theorem liminflimsupxrre

Description: A sequence with values in the extended reals, and with real liminf and limsup, is eventually real. (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses liminflimsupxrre.1 
|- ( ph -> M e. ZZ )
liminflimsupxrre.2 
|- Z = ( ZZ>= ` M )
liminflimsupxrre.3 
|- ( ph -> F : Z --> RR* )
liminflimsupxrre.4 
|- ( ph -> ( limsup ` F ) =/= +oo )
liminflimsupxrre.5 
|- ( ph -> ( liminf ` F ) =/= -oo )
Assertion liminflimsupxrre 
|- ( ph -> E. k e. Z ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> RR )

Proof

Step Hyp Ref Expression
1 liminflimsupxrre.1 
 |-  ( ph -> M e. ZZ )
2 liminflimsupxrre.2 
 |-  Z = ( ZZ>= ` M )
3 liminflimsupxrre.3 
 |-  ( ph -> F : Z --> RR* )
4 liminflimsupxrre.4 
 |-  ( ph -> ( limsup ` F ) =/= +oo )
5 liminflimsupxrre.5 
 |-  ( ph -> ( liminf ` F ) =/= -oo )
6 simpll 
 |-  ( ( ( ph /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> ph )
7 2 uztrn2 
 |-  ( ( k e. Z /\ j e. ( ZZ>= ` k ) ) -> j e. Z )
8 7 adantll 
 |-  ( ( ( ph /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> j e. Z )
9 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
10 3 fdmd 
 |-  ( ph -> dom F = Z )
11 10 adantr 
 |-  ( ( ph /\ j e. Z ) -> dom F = Z )
12 9 11 eleqtrrd 
 |-  ( ( ph /\ j e. Z ) -> j e. dom F )
13 12 ad2antrr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) < +oo ) /\ -oo < ( F ` j ) ) -> j e. dom F )
14 3 ffvelcdmda 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR* )
15 14 ad2antrr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) < +oo ) /\ -oo < ( F ` j ) ) -> ( F ` j ) e. RR* )
16 mnfxr 
 |-  -oo e. RR*
17 16 a1i 
 |-  ( ( ( ph /\ j e. Z ) /\ -oo < ( F ` j ) ) -> -oo e. RR* )
18 14 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ -oo < ( F ` j ) ) -> ( F ` j ) e. RR* )
19 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ -oo < ( F ` j ) ) -> -oo < ( F ` j ) )
20 17 18 19 xrgtned 
 |-  ( ( ( ph /\ j e. Z ) /\ -oo < ( F ` j ) ) -> ( F ` j ) =/= -oo )
21 20 adantlr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) < +oo ) /\ -oo < ( F ` j ) ) -> ( F ` j ) =/= -oo )
22 14 adantr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F ` j ) < +oo ) -> ( F ` j ) e. RR* )
23 pnfxr 
 |-  +oo e. RR*
24 23 a1i 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F ` j ) < +oo ) -> +oo e. RR* )
25 simpr 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F ` j ) < +oo ) -> ( F ` j ) < +oo )
26 22 24 25 xrltned 
 |-  ( ( ( ph /\ j e. Z ) /\ ( F ` j ) < +oo ) -> ( F ` j ) =/= +oo )
27 26 adantr 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) < +oo ) /\ -oo < ( F ` j ) ) -> ( F ` j ) =/= +oo )
28 15 21 27 xrred 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) < +oo ) /\ -oo < ( F ` j ) ) -> ( F ` j ) e. RR )
29 13 28 jca 
 |-  ( ( ( ( ph /\ j e. Z ) /\ ( F ` j ) < +oo ) /\ -oo < ( F ` j ) ) -> ( j e. dom F /\ ( F ` j ) e. RR ) )
30 29 expl 
 |-  ( ( ph /\ j e. Z ) -> ( ( ( F ` j ) < +oo /\ -oo < ( F ` j ) ) -> ( j e. dom F /\ ( F ` j ) e. RR ) ) )
31 6 8 30 syl2anc 
 |-  ( ( ( ph /\ k e. Z ) /\ j e. ( ZZ>= ` k ) ) -> ( ( ( F ` j ) < +oo /\ -oo < ( F ` j ) ) -> ( j e. dom F /\ ( F ` j ) e. RR ) ) )
32 31 ralimdva 
 |-  ( ( ph /\ k e. Z ) -> ( A. j e. ( ZZ>= ` k ) ( ( F ` j ) < +oo /\ -oo < ( F ` j ) ) -> A. j e. ( ZZ>= ` k ) ( j e. dom F /\ ( F ` j ) e. RR ) ) )
33 32 imp 
 |-  ( ( ( ph /\ k e. Z ) /\ A. j e. ( ZZ>= ` k ) ( ( F ` j ) < +oo /\ -oo < ( F ` j ) ) ) -> A. j e. ( ZZ>= ` k ) ( j e. dom F /\ ( F ` j ) e. RR ) )
34 3 ffund 
 |-  ( ph -> Fun F )
35 ffvresb 
 |-  ( Fun F -> ( ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> RR <-> A. j e. ( ZZ>= ` k ) ( j e. dom F /\ ( F ` j ) e. RR ) ) )
36 34 35 syl 
 |-  ( ph -> ( ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> RR <-> A. j e. ( ZZ>= ` k ) ( j e. dom F /\ ( F ` j ) e. RR ) ) )
37 36 ad2antrr 
 |-  ( ( ( ph /\ k e. Z ) /\ A. j e. ( ZZ>= ` k ) ( ( F ` j ) < +oo /\ -oo < ( F ` j ) ) ) -> ( ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> RR <-> A. j e. ( ZZ>= ` k ) ( j e. dom F /\ ( F ` j ) e. RR ) ) )
38 33 37 mpbird 
 |-  ( ( ( ph /\ k e. Z ) /\ A. j e. ( ZZ>= ` k ) ( ( F ` j ) < +oo /\ -oo < ( F ` j ) ) ) -> ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> RR )
39 nfv 
 |-  F/ j ph
40 nfcv 
 |-  F/_ j F
41 39 40 1 2 3 4 limsupubuz2 
 |-  ( ph -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) < +oo )
42 39 40 1 2 3 5 liminflbuz2 
 |-  ( ph -> E. k e. Z A. j e. ( ZZ>= ` k ) -oo < ( F ` j ) )
43 2 rexanuz2 
 |-  ( E. k e. Z A. j e. ( ZZ>= ` k ) ( ( F ` j ) < +oo /\ -oo < ( F ` j ) ) <-> ( E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) < +oo /\ E. k e. Z A. j e. ( ZZ>= ` k ) -oo < ( F ` j ) ) )
44 41 42 43 sylanbrc 
 |-  ( ph -> E. k e. Z A. j e. ( ZZ>= ` k ) ( ( F ` j ) < +oo /\ -oo < ( F ` j ) ) )
45 38 44 reximddv3 
 |-  ( ph -> E. k e. Z ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> RR )