Metamath Proof Explorer

Theorem limsupre

Description: If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypotheses limsupre.1 
|- ( ph -> B C_ RR )
limsupre.2 
|- ( ph -> sup ( B , RR* , < ) = +oo )
limsupre.f 
|- ( ph -> F : B --> RR )
limsupre.bnd 
|- ( ph -> E. b e. RR E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )
Assertion limsupre 
|- ( ph -> ( limsup ` F ) e. RR )

Proof

Step Hyp Ref Expression
1 limsupre.1 
 |-  ( ph -> B C_ RR )
2 limsupre.2 
 |-  ( ph -> sup ( B , RR* , < ) = +oo )
3 limsupre.f 
 |-  ( ph -> F : B --> RR )
4 limsupre.bnd 
 |-  ( ph -> E. b e. RR E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )
5 mnfxr 
 |-  -oo e. RR*
6 5 a1i 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> -oo e. RR* )
7 renegcl 
 |-  ( b e. RR -> -u b e. RR )
8 7 rexrd 
 |-  ( b e. RR -> -u b e. RR* )
9 8 ad2antlr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> -u b e. RR* )
10 reex 
 |-  RR e. _V
11 10 a1i 
 |-  ( ph -> RR e. _V )
12 11 1 ssexd 
 |-  ( ph -> B e. _V )
13 fex 
 |-  ( ( F : B --> RR /\ B e. _V ) -> F e. _V )
14 3 12 13 syl2anc 
 |-  ( ph -> F e. _V )
15 limsupcl 
 |-  ( F e. _V -> ( limsup ` F ) e. RR* )
16 14 15 syl 
 |-  ( ph -> ( limsup ` F ) e. RR* )
17 16 ad2antrr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( limsup ` F ) e. RR* )
18 7 mnfltd 
 |-  ( b e. RR -> -oo < -u b )
19 18 ad2antlr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> -oo < -u b )
20 1 ad2antrr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> B C_ RR )
21 ressxr 
 |-  RR C_ RR*
22 21 a1i 
 |-  ( ph -> RR C_ RR* )
23 3 22 fssd 
 |-  ( ph -> F : B --> RR* )
24 23 ad2antrr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> F : B --> RR* )
25 2 ad2antrr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> sup ( B , RR* , < ) = +oo )
26 simpr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )
27 nfv 
 |-  F/ k ( ph /\ b e. RR )
28 nfre1 
 |-  F/ k E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b )
29 27 28 nfan 
 |-  F/ k ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )
30 nfv 
 |-  F/ j ( ph /\ b e. RR )
31 nfv 
 |-  F/ j k e. RR
32 nfra1 
 |-  F/ j A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b )
33 30 31 32 nf3an 
 |-  F/ j ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )
34 simp13 
 |-  ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )
35 simp2 
 |-  ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> j e. B )
36 simp3 
 |-  ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> k <_ j )
37 rspa 
 |-  ( ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) /\ j e. B ) -> ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )
38 37 imp 
 |-  ( ( ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) /\ j e. B ) /\ k <_ j ) -> ( abs ` ( F ` j ) ) <_ b )
39 34 35 36 38 syl21anc 
 |-  ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ( abs ` ( F ` j ) ) <_ b )
40 simp11l 
 |-  ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ph )
41 3 ffvelrnda 
 |-  ( ( ph /\ j e. B ) -> ( F ` j ) e. RR )
42 40 35 41 syl2anc 
 |-  ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ( F ` j ) e. RR )
43 simp11r 
 |-  ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> b e. RR )
44 42 43 absled 
 |-  ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ( ( abs ` ( F ` j ) ) <_ b <-> ( -u b <_ ( F ` j ) /\ ( F ` j ) <_ b ) ) )
45 39 44 mpbid 
 |-  ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ( -u b <_ ( F ` j ) /\ ( F ` j ) <_ b ) )
46 45 simpld 
 |-  ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> -u b <_ ( F ` j ) )
47 46 3exp 
 |-  ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( j e. B -> ( k <_ j -> -u b <_ ( F ` j ) ) ) )
48 33 47 ralrimi 
 |-  ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) )
49 48 3exp 
 |-  ( ( ph /\ b e. RR ) -> ( k e. RR -> ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) ) )
50 49 adantr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( k e. RR -> ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) ) )
51 29 50 reximdai 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> E. k e. RR A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) )
52 26 51 mpd 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> E. k e. RR A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) )
53 breq2 
 |-  ( i = j -> ( h <_ i <-> h <_ j ) )
54 fveq2 
 |-  ( i = j -> ( F ` i ) = ( F ` j ) )
55 54 breq2d 
 |-  ( i = j -> ( -u b <_ ( F ` i ) <-> -u b <_ ( F ` j ) ) )
56 53 55 imbi12d 
 |-  ( i = j -> ( ( h <_ i -> -u b <_ ( F ` i ) ) <-> ( h <_ j -> -u b <_ ( F ` j ) ) ) )
57 56 cbvralvw 
 |-  ( A. i e. B ( h <_ i -> -u b <_ ( F ` i ) ) <-> A. j e. B ( h <_ j -> -u b <_ ( F ` j ) ) )
58 breq1 
 |-  ( h = k -> ( h <_ j <-> k <_ j ) )
59 58 imbi1d 
 |-  ( h = k -> ( ( h <_ j -> -u b <_ ( F ` j ) ) <-> ( k <_ j -> -u b <_ ( F ` j ) ) ) )
60 59 ralbidv 
 |-  ( h = k -> ( A. j e. B ( h <_ j -> -u b <_ ( F ` j ) ) <-> A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) )
61 57 60 syl5bb 
 |-  ( h = k -> ( A. i e. B ( h <_ i -> -u b <_ ( F ` i ) ) <-> A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) ) )
62 61 cbvrexvw 
 |-  ( E. h e. RR A. i e. B ( h <_ i -> -u b <_ ( F ` i ) ) <-> E. k e. RR A. j e. B ( k <_ j -> -u b <_ ( F ` j ) ) )
63 52 62 sylibr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> E. h e. RR A. i e. B ( h <_ i -> -u b <_ ( F ` i ) ) )
64 20 24 9 25 63 limsupbnd2 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> -u b <_ ( limsup ` F ) )
65 6 9 17 19 64 xrltletrd 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> -oo < ( limsup ` F ) )
66 65 4 r19.29a 
 |-  ( ph -> -oo < ( limsup ` F ) )
67 rexr 
 |-  ( b e. RR -> b e. RR* )
68 67 ad2antlr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> b e. RR* )
69 pnfxr 
 |-  +oo e. RR*
70 69 a1i 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> +oo e. RR* )
71 45 simprd 
 |-  ( ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) /\ j e. B /\ k <_ j ) -> ( F ` j ) <_ b )
72 71 3exp 
 |-  ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( j e. B -> ( k <_ j -> ( F ` j ) <_ b ) ) )
73 33 72 ralrimi 
 |-  ( ( ( ph /\ b e. RR ) /\ k e. RR /\ A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> A. j e. B ( k <_ j -> ( F ` j ) <_ b ) )
74 73 3exp 
 |-  ( ( ph /\ b e. RR ) -> ( k e. RR -> ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) ) )
75 74 adantr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( k e. RR -> ( A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) ) )
76 29 75 reximdai 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) -> E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) )
77 26 76 mpd 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ b ) )
78 54 breq1d 
 |-  ( i = j -> ( ( F ` i ) <_ b <-> ( F ` j ) <_ b ) )
79 53 78 imbi12d 
 |-  ( i = j -> ( ( h <_ i -> ( F ` i ) <_ b ) <-> ( h <_ j -> ( F ` j ) <_ b ) ) )
80 79 cbvralvw 
 |-  ( A. i e. B ( h <_ i -> ( F ` i ) <_ b ) <-> A. j e. B ( h <_ j -> ( F ` j ) <_ b ) )
81 58 imbi1d 
 |-  ( h = k -> ( ( h <_ j -> ( F ` j ) <_ b ) <-> ( k <_ j -> ( F ` j ) <_ b ) ) )
82 81 ralbidv 
 |-  ( h = k -> ( A. j e. B ( h <_ j -> ( F ` j ) <_ b ) <-> A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) )
83 80 82 syl5bb 
 |-  ( h = k -> ( A. i e. B ( h <_ i -> ( F ` i ) <_ b ) <-> A. j e. B ( k <_ j -> ( F ` j ) <_ b ) ) )
84 83 cbvrexvw 
 |-  ( E. h e. RR A. i e. B ( h <_ i -> ( F ` i ) <_ b ) <-> E. k e. RR A. j e. B ( k <_ j -> ( F ` j ) <_ b ) )
85 77 84 sylibr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> E. h e. RR A. i e. B ( h <_ i -> ( F ` i ) <_ b ) )
86 20 24 68 85 limsupbnd1 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( limsup ` F ) <_ b )
87 ltpnf 
 |-  ( b e. RR -> b < +oo )
88 87 ad2antlr 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> b < +oo )
89 17 68 70 86 88 xrlelttrd 
 |-  ( ( ( ph /\ b e. RR ) /\ E. k e. RR A. j e. B ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) ) -> ( limsup ` F ) < +oo )
90 89 4 r19.29a 
 |-  ( ph -> ( limsup ` F ) < +oo )
91 xrrebnd 
 |-  ( ( limsup ` F ) e. RR* -> ( ( limsup ` F ) e. RR <-> ( -oo < ( limsup ` F ) /\ ( limsup ` F ) < +oo ) ) )
92 16 91 syl 
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( -oo < ( limsup ` F ) /\ ( limsup ` F ) < +oo ) ) )
93 66 90 92 mpbir2and 
 |-  ( ph -> ( limsup ` F ) e. RR )