Metamath Proof Explorer

Theorem limsuppnflem

Description: If the restriction of a function to every upper interval is unbounded above, its limsup is +oo . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 limsuppnflem.j 
 |-  F/_ j F
2 limsuppnflem.a 
 |-  ( ph -> A C_ RR )
3 limsuppnflem.f 
 |-  ( ph -> F : A --> RR* )
4 id 
 |-  ( ph -> ph )
5 imnan 
 |-  ( ( k <_ j -> -. x <_ ( F ` j ) ) <-> -. ( k <_ j /\ x <_ ( F ` j ) ) )
6 5 ralbii 
 |-  ( A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) <-> A. j e. A -. ( k <_ j /\ x <_ ( F ` j ) ) )
7 ralnex 
 |-  ( A. j e. A -. ( k <_ j /\ x <_ ( F ` j ) ) <-> -. E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
8 6 7 bitri 
 |-  ( A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) <-> -. E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
9 8 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 ) ) )
10 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 ) ) )
11 9 10 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 ) ) )
12 11 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 ) ) )
13 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 ) ) )
14 12 13 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 ) ) )
15 14 biimpri 
 |-  ( -. 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 -> -. x <_ ( F ` j ) ) )
16 simp1 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ ( k <_ j -> -. x <_ ( F ` j ) ) /\ k <_ j ) -> ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) )
17 id 
 |-  ( ( k <_ j -> -. x <_ ( F ` j ) ) -> ( k <_ j -> -. x <_ ( F ` j ) ) )
18 17 imp 
 |-  ( ( ( k <_ j -> -. x <_ ( F ` j ) ) /\ k <_ j ) -> -. x <_ ( F ` j ) )
19 18 3adant1 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ ( k <_ j -> -. x <_ ( F ` j ) ) /\ k <_ j ) -> -. x <_ ( F ` j ) )
20 3 ffvelcdmda 
 |-  ( ( ph /\ j e. A ) -> ( F ` j ) e. RR* )
21 20 ad4ant14 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) -> ( F ` j ) e. RR* )
22 21 adantr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ -. x <_ ( F ` j ) ) -> ( F ` j ) e. RR* )
23 simpllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) -> x e. RR )
24 rexr 
 |-  ( x e. RR -> x e. RR* )
25 23 24 syl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) -> x e. RR* )
26 25 adantr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ -. x <_ ( F ` j ) ) -> x e. RR* )
27 simpr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ -. x <_ ( F ` j ) ) -> -. x <_ ( F ` j ) )
28 20 ad4ant13 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ -. x <_ ( F ` j ) ) -> ( F ` j ) e. RR* )
29 24 ad3antlr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ -. x <_ ( F ` j ) ) -> x e. RR* )
30 28 29 xrltnled 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ -. x <_ ( F ` j ) ) -> ( ( F ` j ) < x <-> -. x <_ ( F ` j ) ) )
31 27 30 mpbird 
 |-  ( ( ( ( ph /\ x e. RR ) /\ j e. A ) /\ -. x <_ ( F ` j ) ) -> ( F ` j ) < x )
32 31 adantllr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ -. x <_ ( F ` j ) ) -> ( F ` j ) < x )
33 22 26 32 xrltled 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ -. x <_ ( F ` j ) ) -> ( F ` j ) <_ x )
34 16 19 33 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ ( k <_ j -> -. x <_ ( F ` j ) ) /\ k <_ j ) -> ( F ` j ) <_ x )
35 34 3exp 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) -> ( ( k <_ j -> -. x <_ ( F ` j ) ) -> ( k <_ j -> ( F ` j ) <_ x ) ) )
36 35 ralimdva 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. RR ) -> ( A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) -> A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
37 36 reximdva 
 |-  ( ( ph /\ x e. RR ) -> ( E. k e. RR A. j e. A ( k <_ j -> -. x <_ ( F ` j ) ) -> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
38 37 reximdva 
 |-  ( ph -> ( E. x e. RR E. k e. RR A. 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 ) ) )
39 38 imp 
 |-  ( ( ph /\ E. x e. RR E. k e. RR A. 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 ) )
40 4 15 39 syl2an 
 |-  ( ( 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 ) )
41 reex 
 |-  RR e. _V
42 41 a1i 
 |-  ( ph -> RR e. _V )
43 42 2 ssexd 
 |-  ( ph -> A e. _V )
44 3 43 fexd 
 |-  ( ph -> F e. _V )
45 44 limsupcld 
 |-  ( ph -> ( limsup ` F ) e. RR* )
46 45 ad2antrr 
 |-  ( ( ( ph /\ x e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> ( limsup ` F ) e. RR* )
47 24 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> x e. RR* )
48 pnfxr 
 |-  +oo e. RR*
49 48 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> +oo e. RR* )
50 2 ad2antrr 
 |-  ( ( ( ph /\ x e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> A C_ RR )
51 3 ad2antrr 
 |-  ( ( ( ph /\ x e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> F : A --> RR* )
52 simpr 
 |-  ( ( ( 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 ) )
53 1 50 51 47 52 limsupbnd1f 
 |-  ( ( ( ph /\ x e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> ( limsup ` F ) <_ x )
54 ltpnf 
 |-  ( x e. RR -> x < +oo )
55 54 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> x < +oo )
56 46 47 49 53 55 xrlelttrd 
 |-  ( ( ( ph /\ x e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> ( limsup ` F ) < +oo )
57 56 rexlimdva2 
 |-  ( ph -> ( E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) -> ( limsup ` F ) < +oo ) )
58 57 imp 
 |-  ( ( ph /\ E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> ( limsup ` F ) < +oo )
59 40 58 syldan 
 |-  ( ( ph /\ -. A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) -> ( limsup ` F ) < +oo )
60 59 adantlr 
 |-  ( ( ( ph /\ ( limsup ` F ) = +oo ) /\ -. A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) -> ( limsup ` F ) < +oo )
61 id 
 |-  ( ( limsup ` F ) = +oo -> ( limsup ` F ) = +oo )
62 48 a1i 
 |-  ( ( limsup ` F ) = +oo -> +oo e. RR* )
63 61 62 eqeltrd 
 |-  ( ( limsup ` F ) = +oo -> ( limsup ` F ) e. RR* )
64 63 61 xreqnltd 
 |-  ( ( limsup ` F ) = +oo -> -. ( limsup ` F ) < +oo )
65 64 adantl 
 |-  ( ( ph /\ ( limsup ` F ) = +oo ) -> -. ( limsup ` F ) < +oo )
66 65 adantr 
 |-  ( ( ( ph /\ ( limsup ` F ) = +oo ) /\ -. A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) -> -. ( limsup ` F ) < +oo )
67 60 66 condan 
 |-  ( ( ph /\ ( limsup ` F ) = +oo ) -> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
68 67 ex 
 |-  ( ph -> ( ( limsup ` F ) = +oo -> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )
69 2 adantr 
 |-  ( ( ph /\ A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) -> A C_ RR )
70 3 adantr 
 |-  ( ( ph /\ A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) -> F : A --> RR* )
71 simpr 
 |-  ( ( 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 ) ) )
72 1 69 70 71 limsuppnfd 
 |-  ( ( ph /\ A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) -> ( limsup ` F ) = +oo )
73 72 ex 
 |-  ( ph -> ( A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) -> ( limsup ` F ) = +oo ) )
74 68 73 impbid 
 |-  ( ph -> ( ( limsup ` F ) = +oo <-> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) ) )