Metamath Proof Explorer

Theorem limsupub

Description: If the limsup is not +oo , then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupub.j 
|- F/ j ph
limsupub.e 
|- F/_ j F
limsupub.a 
|- ( ph -> A C_ RR )
limsupub.f 
|- ( ph -> F : A --> RR* )
limsupub.n 
|- ( ph -> ( limsup ` F ) =/= +oo )
Assertion limsupub 
|- ( ph -> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )

Proof

Step Hyp Ref Expression
1 limsupub.j 
 |-  F/ j ph
2 limsupub.e 
 |-  F/_ j F
3 limsupub.a 
 |-  ( ph -> A C_ RR )
4 limsupub.f 
 |-  ( ph -> F : A --> RR* )
5 limsupub.n 
 |-  ( ph -> ( limsup ` F ) =/= +oo )
6 3 adantr 
 |-  ( ( ph /\ A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) ) -> A C_ RR )
7 4 adantr 
 |-  ( ( ph /\ A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) ) -> F : A --> RR* )
8 nfv 
 |-  F/ j x e. RR
9 1 8 nfan 
 |-  F/ j ( ph /\ x e. RR )
10 simprl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ ( k <_ j /\ x < ( F ` j ) ) ) -> k <_ j )
11 simpllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ x < ( F ` j ) ) -> x e. RR )
12 rexr 
 |-  ( x e. RR -> x e. RR* )
13 11 12 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ x < ( F ` j ) ) -> x e. RR* )
14 4 ffvelrnda 
 |-  ( ( ph /\ j e. A ) -> ( F ` j ) e. RR* )
15 14 ad4ant13 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ x < ( F ` j ) ) -> ( F ` j ) e. RR* )
16 simpr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ x < ( F ` j ) ) -> x < ( F ` j ) )
17 13 15 16 xrltled 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ x < ( F ` j ) ) -> x <_ ( F ` j ) )
18 17 adantrl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ ( k <_ j /\ x < ( F ` j ) ) ) -> x <_ ( F ` j ) )
19 10 18 jca 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ ( k <_ j /\ x < ( F ` j ) ) ) -> ( k <_ j /\ x <_ ( F ` j ) ) )
20 19 ex 
 |-  ( ( ( ph /\ x e. RR ) /\ j e. A ) -> ( ( k <_ j /\ x < ( F ` j ) ) -> ( k <_ j /\ x <_ ( F ` j ) ) ) )
21 20 ex 
 |-  ( ( ph /\ x e. RR ) -> ( j e. A -> ( ( k <_ j /\ x < ( F ` j ) ) -> ( k <_ j /\ x <_ ( F ` j ) ) ) ) )
22 9 21 reximdai 
 |-  ( ( ph /\ x e. RR ) -> ( E. j e. A ( k <_ j /\ x < ( F ` j ) ) -> E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
23 22 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 <_ ( F ` j ) ) ) )
24 23 ralimdva 
 |-  ( ph -> ( A. 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 ) ) ) )
25 24 imp 
 |-  ( ( ph /\ A. 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 ) ) )
26 2 6 7 25 limsuppnfd 
 |-  ( ( ph /\ A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) ) -> ( limsup ` F ) = +oo )
27 5 neneqd 
 |-  ( ph -> -. ( limsup ` F ) = +oo )
28 27 adantr 
 |-  ( ( ph /\ A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) ) -> -. ( limsup ` F ) = +oo )
29 26 28 pm2.65da 
 |-  ( ph -> -. A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x < ( F ` j ) ) )
30 imnan 
 |-  ( ( k <_ j -> -. x < ( F ` j ) ) <-> -. ( k <_ j /\ x < ( F ` j ) ) )
31 30 ralbii 
 |-  ( A. j e. A ( k <_ j -> -. x < ( F ` j ) ) <-> A. j e. A -. ( k <_ j /\ x < ( F ` j ) ) )
32 ralnex 
 |-  ( A. j e. A -. ( k <_ j /\ x < ( F ` j ) ) <-> -. E. j e. A ( k <_ j /\ x < ( F ` j ) ) )
33 31 32 bitri 
 |-  ( A. j e. A ( k <_ j -> -. x < ( F ` j ) ) <-> -. E. j e. A ( k <_ j /\ x < ( F ` j ) ) )
34 33 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 ) ) )
35 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 ) ) )
36 34 35 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 ) ) )
37 36 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 ) ) )
38 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 ) ) )
39 37 38 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 ) ) )
40 29 39 sylibr 
 |-  ( ph -> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> -. x < ( F ` j ) ) )
41 nfv 
 |-  F/ j k e. RR
42 9 41 nfan 
 |-  F/ j ( ( ph /\ x e. RR ) /\ k e. RR )
43 14 ad4ant14 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) -> ( F ` j ) e. RR* )
44 simpllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) -> x e. RR )
45 44 rexrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) -> x e. RR* )
46 43 45 xrlenltd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) -> ( ( F ` j ) <_ x <-> -. x < ( F ` j ) ) )
47 46 imbi2d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) -> ( ( k <_ j -> ( F ` j ) <_ x ) <-> ( k <_ j -> -. x < ( F ` j ) ) ) )
48 42 47 ralbida 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. RR ) -> ( A. j e. A ( k <_ j -> ( F ` j ) <_ x ) <-> A. j e. A ( k <_ j -> -. x < ( F ` j ) ) ) )
49 48 rexbidva 
 |-  ( ( 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 ) ) ) )
50 49 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 ) ) ) )
51 40 50 mpbird 
 |-  ( ph -> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )