Metamath Proof Explorer

Theorem limsupre3uz

Description: Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, infinitely often; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupre3uz.1 
|- F/_ j F
limsupre3uz.2 
|- ( ph -> M e. ZZ )
limsupre3uz.3 
|- Z = ( ZZ>= ` M )
limsupre3uz.4 
|- ( ph -> F : Z --> RR* )
Assertion limsupre3uz 
|- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )

Proof

Step Hyp Ref Expression
1 limsupre3uz.1 
 |-  F/_ j F
2 limsupre3uz.2 
 |-  ( ph -> M e. ZZ )
3 limsupre3uz.3 
 |-  Z = ( ZZ>= ` M )
4 limsupre3uz.4 
 |-  ( ph -> F : Z --> RR* )
5 nfcv 
 |-  F/_ l F
6 5 2 3 4 limsupre3uzlem 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. y e. RR A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) /\ E. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) ) )
7 breq1 
 |-  ( y = x -> ( y <_ ( F ` l ) <-> x <_ ( F ` l ) ) )
8 7 rexbidv 
 |-  ( y = x -> ( E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) ) )
9 8 ralbidv 
 |-  ( y = x -> ( A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> A. i e. Z E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) ) )
10 fveq2 
 |-  ( i = k -> ( ZZ>= ` i ) = ( ZZ>= ` k ) )
11 10 rexeqdv 
 |-  ( i = k -> ( E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> E. l e. ( ZZ>= ` k ) x <_ ( F ` l ) ) )
12 nfcv 
 |-  F/_ j x
13 nfcv 
 |-  F/_ j <_
14 nfcv 
 |-  F/_ j l
15 1 14 nffv 
 |-  F/_ j ( F ` l )
16 12 13 15 nfbr 
 |-  F/ j x <_ ( F ` l )
17 nfv 
 |-  F/ l x <_ ( F ` j )
18 fveq2 
 |-  ( l = j -> ( F ` l ) = ( F ` j ) )
19 18 breq2d 
 |-  ( l = j -> ( x <_ ( F ` l ) <-> x <_ ( F ` j ) ) )
20 16 17 19 cbvrexw 
 |-  ( E. l e. ( ZZ>= ` k ) x <_ ( F ` l ) <-> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
21 20 a1i 
 |-  ( i = k -> ( E. l e. ( ZZ>= ` k ) x <_ ( F ` l ) <-> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
22 11 21 bitrd 
 |-  ( i = k -> ( E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
23 22 cbvralvw 
 |-  ( A. i e. Z E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
24 23 a1i 
 |-  ( y = x -> ( A. i e. Z E. l e. ( ZZ>= ` i ) x <_ ( F ` l ) <-> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
25 9 24 bitrd 
 |-  ( y = x -> ( A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
26 25 cbvrexvw 
 |-  ( E. y e. RR A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
27 breq2 
 |-  ( y = x -> ( ( F ` l ) <_ y <-> ( F ` l ) <_ x ) )
28 27 ralbidv 
 |-  ( y = x -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x ) )
29 28 rexbidv 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x ) )
30 10 raleqdv 
 |-  ( i = k -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. l e. ( ZZ>= ` k ) ( F ` l ) <_ x ) )
31 15 13 12 nfbr 
 |-  F/ j ( F ` l ) <_ x
32 nfv 
 |-  F/ l ( F ` j ) <_ x
33 18 breq1d 
 |-  ( l = j -> ( ( F ` l ) <_ x <-> ( F ` j ) <_ x ) )
34 31 32 33 cbvralw 
 |-  ( A. l e. ( ZZ>= ` k ) ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
35 34 a1i 
 |-  ( i = k -> ( A. l e. ( ZZ>= ` k ) ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
36 30 35 bitrd 
 |-  ( i = k -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
37 36 cbvrexvw 
 |-  ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
38 37 a1i 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
39 29 38 bitrd 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
40 39 cbvrexvw 
 |-  ( E. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
41 26 40 anbi12i 
 |-  ( ( E. y e. RR A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) /\ E. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
42 41 a1i 
 |-  ( ph -> ( ( E. y e. RR A. i e. Z E. l e. ( ZZ>= ` i ) y <_ ( F ` l ) /\ E. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )
43 6 42 bitrd 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )