Metamath Proof Explorer

Theorem limsupre3lem

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, at some point, in any upper part of the reals; 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 limsupre3lem.1 
|- F/_ j F
limsupre3lem.2 
|- ( ph -> A C_ RR )
limsupre3lem.3 
|- ( ph -> F : A --> RR* )
Assertion limsupre3lem 
|- ( 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 limsupre3lem.1 
 |-  F/_ j F
2 limsupre3lem.2 
 |-  ( ph -> A C_ RR )
3 limsupre3lem.3 
 |-  ( ph -> F : A --> RR* )
4 1 2 3 limsupre2 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. y e. RR A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) /\ E. y e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) ) ) )
5 simp2 
 |-  ( ( ph /\ y e. RR /\ A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) ) -> y e. RR )
6 nfv 
 |-  F/ j ( ph /\ y e. RR )
7 simp3l 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. A /\ ( k <_ j /\ y < ( F ` j ) ) ) -> k <_ j )
8 simp1r 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. A /\ y < ( F ` j ) ) -> y e. RR )
9 8 rexrd 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. A /\ y < ( F ` j ) ) -> y e. RR* )
10 3 ffvelrnda 
 |-  ( ( ph /\ j e. A ) -> ( F ` j ) e. RR* )
11 10 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. A ) -> ( F ` j ) e. RR* )
12 11 3adant3 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. A /\ y < ( F ` j ) ) -> ( F ` j ) e. RR* )
13 simp3 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. A /\ y < ( F ` j ) ) -> y < ( F ` j ) )
14 9 12 13 xrltled 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. A /\ y < ( F ` j ) ) -> y <_ ( F ` j ) )
15 14 3adant3l 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. A /\ ( k <_ j /\ y < ( F ` j ) ) ) -> y <_ ( F ` j ) )
16 7 15 jca 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. A /\ ( k <_ j /\ y < ( F ` j ) ) ) -> ( k <_ j /\ y <_ ( F ` j ) ) )
17 16 3exp 
 |-  ( ( ph /\ y e. RR ) -> ( j e. A -> ( ( k <_ j /\ y < ( F ` j ) ) -> ( k <_ j /\ y <_ ( F ` j ) ) ) ) )
18 6 17 reximdai 
 |-  ( ( ph /\ y e. RR ) -> ( E. j e. A ( k <_ j /\ y < ( F ` j ) ) -> E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) ) )
19 18 ralimdv 
 |-  ( ( ph /\ y e. RR ) -> ( A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) -> A. k e. RR E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) ) )
20 19 3impia 
 |-  ( ( ph /\ y e. RR /\ A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) ) -> A. k e. RR E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) )
21 breq1 
 |-  ( x = y -> ( x <_ ( F ` j ) <-> y <_ ( F ` j ) ) )
22 21 anbi2d 
 |-  ( x = y -> ( ( k <_ j /\ x <_ ( F ` j ) ) <-> ( k <_ j /\ y <_ ( F ` j ) ) ) )
23 22 rexbidv 
 |-  ( x = y -> ( E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) <-> E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) ) )
24 23 ralbidv 
 |-  ( x = y -> ( A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) ) )
25 24 rspcev 
 |-  ( ( y e. RR /\ A. k e. RR E. j e. A ( k <_ j /\ y <_ ( F ` j ) ) ) -> E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
26 5 20 25 syl2anc 
 |-  ( ( ph /\ y e. RR /\ A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) ) -> E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
27 26 3exp 
 |-  ( ph -> ( y e. RR -> ( A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) -> E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) ) )
28 27 rexlimdv 
 |-  ( ph -> ( E. y e. RR A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) -> E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
29 peano2rem 
 |-  ( x e. RR -> ( x - 1 ) e. RR )
30 29 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) -> ( x - 1 ) e. RR )
31 nfv 
 |-  F/ j ( ph /\ x e. RR )
32 simp3l 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> k <_ j )
33 simp1r 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> x e. RR )
34 29 rexrd 
 |-  ( x e. RR -> ( x - 1 ) e. RR* )
35 33 34 syl 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> ( x - 1 ) e. RR* )
36 33 rexrd 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> x e. RR* )
37 10 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> ( F ` j ) e. RR* )
38 37 3adant3 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> ( F ` j ) e. RR* )
39 33 ltm1d 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> ( x - 1 ) < x )
40 simp3r 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> x <_ ( F ` j ) )
41 35 36 38 39 40 xrltletrd 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> ( x - 1 ) < ( F ` j ) )
42 32 41 jca 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> ( k <_ j /\ ( x - 1 ) < ( F ` j ) ) )
43 42 3exp 
 |-  ( ( ph /\ x e. RR ) -> ( j e. A -> ( ( k <_ j /\ x <_ ( F ` j ) ) -> ( k <_ j /\ ( x - 1 ) < ( F ` j ) ) ) ) )
44 31 43 reximdai 
 |-  ( ( ph /\ x e. RR ) -> ( E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) -> E. j e. A ( k <_ j /\ ( x - 1 ) < ( F ` j ) ) ) )
45 44 ralimdv 
 |-  ( ( ph /\ x e. RR ) -> ( A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) -> A. k e. RR E. j e. A ( k <_ j /\ ( x - 1 ) < ( F ` j ) ) ) )
46 45 imp 
 |-  ( ( ( ph /\ x e. RR ) /\ A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) -> A. k e. RR E. j e. A ( k <_ j /\ ( x - 1 ) < ( F ` j ) ) )
47 breq1 
 |-  ( y = ( x - 1 ) -> ( y < ( F ` j ) <-> ( x - 1 ) < ( F ` j ) ) )
48 47 anbi2d 
 |-  ( y = ( x - 1 ) -> ( ( k <_ j /\ y < ( F ` j ) ) <-> ( k <_ j /\ ( x - 1 ) < ( F ` j ) ) ) )
49 48 rexbidv 
 |-  ( y = ( x - 1 ) -> ( E. j e. A ( k <_ j /\ y < ( F ` j ) ) <-> E. j e. A ( k <_ j /\ ( x - 1 ) < ( F ` j ) ) ) )
50 49 ralbidv 
 |-  ( y = ( x - 1 ) -> ( A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) <-> A. k e. RR E. j e. A ( k <_ j /\ ( x - 1 ) < ( F ` j ) ) ) )
51 50 rspcev 
 |-  ( ( ( x - 1 ) e. RR /\ A. k e. RR E. j e. A ( k <_ j /\ ( x - 1 ) < ( F ` j ) ) ) -> E. y e. RR A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) )
52 30 46 51 syl2anc 
 |-  ( ( ( ph /\ x e. RR ) /\ A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) -> E. y e. RR A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) )
53 52 rexlimdva2 
 |-  ( ph -> ( E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) -> E. y e. RR A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) ) )
54 28 53 impbid 
 |-  ( ph -> ( E. y e. RR A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) <-> E. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
55 simplr 
 |-  ( ( ( ph /\ y e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) ) -> y e. RR )
56 11 adantr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ j e. A ) /\ ( F ` j ) < y ) -> ( F ` j ) e. RR* )
57 rexr 
 |-  ( y e. RR -> y e. RR* )
58 57 ad3antlr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ j e. A ) /\ ( F ` j ) < y ) -> y e. RR* )
59 simpr 
 |-  ( ( ( ( ph /\ y e. RR ) /\ j e. A ) /\ ( F ` j ) < y ) -> ( F ` j ) < y )
60 56 58 59 xrltled 
 |-  ( ( ( ( ph /\ y e. RR ) /\ j e. A ) /\ ( F ` j ) < y ) -> ( F ` j ) <_ y )
61 60 ex 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. A ) -> ( ( F ` j ) < y -> ( F ` j ) <_ y ) )
62 61 imim2d 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. A ) -> ( ( k <_ j -> ( F ` j ) < y ) -> ( k <_ j -> ( F ` j ) <_ y ) ) )
63 62 ralimdva 
 |-  ( ( ph /\ y e. RR ) -> ( A. j e. A ( k <_ j -> ( F ` j ) < y ) -> A. j e. A ( k <_ j -> ( F ` j ) <_ y ) ) )
64 63 reximdv 
 |-  ( ( ph /\ y e. RR ) -> ( E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) -> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ y ) ) )
65 64 imp 
 |-  ( ( ( ph /\ y e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) ) -> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ y ) )
66 breq2 
 |-  ( x = y -> ( ( F ` j ) <_ x <-> ( F ` j ) <_ y ) )
67 66 imbi2d 
 |-  ( x = y -> ( ( k <_ j -> ( F ` j ) <_ x ) <-> ( k <_ j -> ( F ` j ) <_ y ) ) )
68 67 ralbidv 
 |-  ( x = y -> ( A. j e. A ( k <_ j -> ( F ` j ) <_ x ) <-> A. j e. A ( k <_ j -> ( F ` j ) <_ y ) ) )
69 68 rexbidv 
 |-  ( x = y -> ( E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) <-> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ y ) ) )
70 69 rspcev 
 |-  ( ( y e. RR /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ y ) ) -> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
71 55 65 70 syl2anc 
 |-  ( ( ( ph /\ y e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) ) -> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
72 71 rexlimdva2 
 |-  ( ph -> ( E. y e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) -> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
73 peano2re 
 |-  ( x e. RR -> ( x + 1 ) e. RR )
74 73 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> ( x + 1 ) e. RR )
75 37 adantr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> ( F ` j ) e. RR* )
76 rexr 
 |-  ( x e. RR -> x e. RR* )
77 76 ad3antlr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> x e. RR* )
78 73 rexrd 
 |-  ( x e. RR -> ( x + 1 ) e. RR* )
79 78 ad3antlr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> ( x + 1 ) e. RR* )
80 simpr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> ( F ` j ) <_ x )
81 ltp1 
 |-  ( x e. RR -> x < ( x + 1 ) )
82 81 ad3antlr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> x < ( x + 1 ) )
83 75 77 79 80 82 xrlelttrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> ( F ` j ) < ( x + 1 ) )
84 83 ex 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> ( ( F ` j ) <_ x -> ( F ` j ) < ( x + 1 ) ) )
85 84 imim2d 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> ( ( k <_ j -> ( F ` j ) <_ x ) -> ( k <_ j -> ( F ` j ) < ( x + 1 ) ) ) )
86 85 ralimdva 
 |-  ( ( ph /\ x e. RR ) -> ( A. j e. A ( k <_ j -> ( F ` j ) <_ x ) -> A. j e. A ( k <_ j -> ( F ` j ) < ( x + 1 ) ) ) )
87 86 reximdv 
 |-  ( ( 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 -> ( F ` j ) < ( x + 1 ) ) ) )
88 87 imp 
 |-  ( ( ( 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 -> ( F ` j ) < ( x + 1 ) ) )
89 breq2 
 |-  ( y = ( x + 1 ) -> ( ( F ` j ) < y <-> ( F ` j ) < ( x + 1 ) ) )
90 89 imbi2d 
 |-  ( y = ( x + 1 ) -> ( ( k <_ j -> ( F ` j ) < y ) <-> ( k <_ j -> ( F ` j ) < ( x + 1 ) ) ) )
91 90 ralbidv 
 |-  ( y = ( x + 1 ) -> ( A. j e. A ( k <_ j -> ( F ` j ) < y ) <-> A. j e. A ( k <_ j -> ( F ` j ) < ( x + 1 ) ) ) )
92 91 rexbidv 
 |-  ( y = ( x + 1 ) -> ( E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) <-> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < ( x + 1 ) ) ) )
93 92 rspcev 
 |-  ( ( ( x + 1 ) e. RR /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < ( x + 1 ) ) ) -> E. y e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) )
94 74 88 93 syl2anc 
 |-  ( ( ( ph /\ x e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> E. y e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) )
95 94 rexlimdva2 
 |-  ( ph -> ( E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) -> E. y e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) ) )
96 72 95 impbid 
 |-  ( ph -> ( E. y e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) <-> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
97 54 96 anbi12d 
 |-  ( ph -> ( ( E. y e. RR A. k e. RR E. j e. A ( k <_ j /\ y < ( F ` j ) ) /\ E. y e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < y ) ) <-> ( 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 ) ) ) )
98 4 97 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 ) ) ) )