Metamath Proof Explorer

Theorem limsupre2lem

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 smaller than the function, at some point, in any upper part of the reals; 2. there is a real number that is eventually larger than the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupre2lem.1 
|- F/_ j F
limsupre2lem.2 
|- ( ph -> A C_ RR )
limsupre2lem.3 
|- ( ph -> F : A --> RR* )
Assertion limsupre2lem 
|- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < x ) ) ) )

Proof

Step Hyp Ref Expression
1 limsupre2lem.1 
 |-  F/_ j F
2 limsupre2lem.2 
 |-  ( ph -> A C_ RR )
3 limsupre2lem.3 
 |-  ( ph -> F : A --> RR* )
4 reex 
 |-  RR e. _V
5 4 a1i 
 |-  ( ph -> RR e. _V )
6 5 2 ssexd 
 |-  ( ph -> A e. _V )
7 3 6 fexd 
 |-  ( ph -> F e. _V )
8 7 limsupcld 
 |-  ( ph -> ( limsup ` F ) e. RR* )
9 xrre4 
 |-  ( ( limsup ` F ) e. RR* -> ( ( limsup ` F ) e. RR <-> ( ( limsup ` F ) =/= -oo /\ ( limsup ` F ) =/= +oo ) ) )
10 8 9 syl 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( ( limsup ` F ) =/= -oo /\ ( limsup ` F ) =/= +oo ) ) )
11 df-ne 
 |-  ( ( limsup ` F ) =/= -oo <-> -. ( limsup ` F ) = -oo )
12 11 a1i 
 |-  ( ph -> ( ( limsup ` F ) =/= -oo <-> -. ( limsup ` F ) = -oo ) )
13 1 2 3 limsupmnf 
 |-  ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
14 13 notbid 
 |-  ( ph -> ( -. ( limsup ` F ) = -oo <-> -. A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
15 annim 
 |-  ( ( k <_ j /\ -. ( F ` j ) <_ x ) <-> -. ( k <_ j -> ( F ` j ) <_ x ) )
16 15 rexbii 
 |-  ( E. j e. A ( k <_ j /\ -. ( F ` j ) <_ x ) <-> E. j e. A -. ( k <_ j -> ( F ` j ) <_ x ) )
17 rexnal 
 |-  ( E. j e. A -. ( k <_ j -> ( F ` j ) <_ x ) <-> -. A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
18 16 17 bitri 
 |-  ( E. j e. A ( k <_ j /\ -. ( F ` j ) <_ x ) <-> -. A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
19 18 ralbii 
 |-  ( A. k e. RR E. j e. A ( k <_ j /\ -. ( F ` j ) <_ x ) <-> A. k e. RR -. A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
20 ralnex 
 |-  ( A. k e. RR -. A. j e. A ( k <_ j -> ( F ` j ) <_ x ) <-> -. E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
21 19 20 bitri 
 |-  ( A. k e. RR E. j e. A ( k <_ j /\ -. ( F ` j ) <_ x ) <-> -. E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
22 21 rexbii 
 |-  ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ -. ( F ` j ) <_ x ) <-> E. x e. RR -. E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
23 rexnal 
 |-  ( E. x e. RR -. E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) <-> -. A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
24 22 23 bitr2i 
 |-  ( -. A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) <-> E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ -. ( F ` j ) <_ x ) )
25 24 a1i 
 |-  ( ph -> ( -. A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) <-> E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ -. ( F ` j ) <_ x ) ) )
26 simplr 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> x e. RR )
27 26 rexrd 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> x e. RR* )
28 3 adantr 
 |-  ( ( ph /\ x e. RR ) -> F : A --> RR* )
29 28 ffvelrnda 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> ( F ` j ) e. RR* )
30 27 29 xrltnled 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> ( x < ( F ` j ) <-> -. ( F ` j ) <_ x ) )
31 30 bicomd 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> ( -. ( F ` j ) <_ x <-> x < ( F ` j ) ) )
32 31 anbi2d 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> ( ( k <_ j /\ -. ( F ` j ) <_ x ) <-> ( k <_ j /\ x < ( F ` j ) ) ) )
33 32 rexbidva 
 |-  ( ( ph /\ x e. RR ) -> ( E. j e. A ( k <_ j /\ -. ( F ` j ) <_ x ) <-> E. j e. A ( k <_ j /\ x < ( F ` j ) ) ) )
34 33 ralbidv 
 |-  ( ( ph /\ x e. RR ) -> ( A. k e. RR E. j e. A ( k <_ j /\ -. ( F ` j ) <_ x ) <-> A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) ) )
35 34 rexbidva 
 |-  ( ph -> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ -. ( F ` j ) <_ x ) <-> E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) ) )
36 25 35 bitrd 
 |-  ( ph -> ( -. A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) <-> E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) ) )
37 12 14 36 3bitrd 
 |-  ( ph -> ( ( limsup ` F ) =/= -oo <-> E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) ) )
38 df-ne 
 |-  ( ( limsup ` F ) =/= +oo <-> -. ( limsup ` F ) = +oo )
39 38 a1i 
 |-  ( ph -> ( ( limsup ` F ) =/= +oo <-> -. ( limsup ` F ) = +oo ) )
40 1 2 3 limsuppnf 
 |-  ( ph -> ( ( limsup ` F ) = +oo <-> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
41 40 notbid 
 |-  ( ph -> ( -. ( limsup ` F ) = +oo <-> -. A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
42 29 27 xrltnled 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> ( ( F ` j ) < x <-> -. x <_ ( F ` j ) ) )
43 42 imbi2d 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> ( ( k <_ j -> ( F ` j ) < x ) <-> ( k <_ j -> -. x <_ ( F ` j ) ) ) )
44 43 ralbidva 
 |-  ( ( ph /\ x e. RR ) -> ( A. j e. A ( k <_ j -> ( F ` j ) < x ) <-> A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) ) )
45 44 rexbidv 
 |-  ( ( ph /\ x e. RR ) -> ( E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < x ) <-> E. k e. RR A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) ) )
46 45 rexbidva 
 |-  ( ph -> ( E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < x ) <-> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) ) )
47 imnan 
 |-  ( ( k <_ j -> -. x <_ ( F ` j ) ) <-> -. ( k <_ j /\ x <_ ( F ` j ) ) )
48 47 ralbii 
 |-  ( A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) <-> A. j e. A -. ( k <_ j /\ x <_ ( F ` j ) ) )
49 ralnex 
 |-  ( A. j e. A -. ( k <_ j /\ x <_ ( F ` j ) ) <-> -. E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
50 48 49 bitri 
 |-  ( A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) <-> -. E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
51 50 rexbii 
 |-  ( E. k e. RR A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) <-> E. k e. RR -. E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
52 rexnal 
 |-  ( E. k e. RR -. E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) <-> -. A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
53 51 52 bitri 
 |-  ( E. k e. RR A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) <-> -. A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
54 53 rexbii 
 |-  ( E. x e. RR E. k e. RR A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) <-> E. x e. RR -. A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
55 rexnal 
 |-  ( E. x e. RR -. A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) <-> -. A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
56 54 55 bitri 
 |-  ( E. x e. RR E. k e. RR A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) <-> -. A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
57 56 a1i 
 |-  ( ph -> ( E. x e. RR E. k e. RR A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) <-> -. A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
58 46 57 bitr2d 
 |-  ( ph -> ( -. A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) <-> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < x ) ) )
59 39 41 58 3bitrd 
 |-  ( ph -> ( ( limsup ` F ) =/= +oo <-> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < x ) ) )
60 37 59 anbi12d 
 |-  ( ph -> ( ( ( limsup ` F ) =/= -oo /\ ( limsup ` F ) =/= +oo ) <-> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < x ) ) ) )
61 10 60 bitrd 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < x ) ) ) )