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