Metamath Proof Explorer

Theorem limsupref

Description: If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupref.j 
|- F/_ j F
limsupref.a 
|- ( ph -> A C_ RR )
limsupref.s 
|- ( ph -> sup ( A , RR* , < ) = +oo )
limsupref.f 
|- ( ph -> F : A --> RR )
limsupref.b 
|- ( ph -> E. b e. RR E. k e. RR A. j e. A ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )
Assertion limsupref 
|- ( ph -> ( limsup ` F ) e. RR )

Proof

Step Hyp Ref Expression
1 limsupref.j 
 |-  F/_ j F
2 limsupref.a 
 |-  ( ph -> A C_ RR )
3 limsupref.s 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
4 limsupref.f 
 |-  ( ph -> F : A --> RR )
5 limsupref.b 
 |-  ( ph -> E. b e. RR E. k e. RR A. j e. A ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) )
6 breq2 
 |-  ( b = y -> ( ( abs ` ( F ` j ) ) <_ b <-> ( abs ` ( F ` j ) ) <_ y ) )
7 6 imbi2d 
 |-  ( b = y -> ( ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) <-> ( k <_ j -> ( abs ` ( F ` j ) ) <_ y ) ) )
8 7 ralbidv 
 |-  ( b = y -> ( A. j e. A ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) <-> A. j e. A ( k <_ j -> ( abs ` ( F ` j ) ) <_ y ) ) )
9 breq1 
 |-  ( k = i -> ( k <_ j <-> i <_ j ) )
10 9 imbi1d 
 |-  ( k = i -> ( ( k <_ j -> ( abs ` ( F ` j ) ) <_ y ) <-> ( i <_ j -> ( abs ` ( F ` j ) ) <_ y ) ) )
11 10 ralbidv 
 |-  ( k = i -> ( A. j e. A ( k <_ j -> ( abs ` ( F ` j ) ) <_ y ) <-> A. j e. A ( i <_ j -> ( abs ` ( F ` j ) ) <_ y ) ) )
12 nfv 
 |-  F/ x ( i <_ j -> ( abs ` ( F ` j ) ) <_ y )
13 nfv 
 |-  F/ j i <_ x
14 nfcv 
 |-  F/_ j abs
15 nfcv 
 |-  F/_ j x
16 1 15 nffv 
 |-  F/_ j ( F ` x )
17 14 16 nffv 
 |-  F/_ j ( abs ` ( F ` x ) )
18 nfcv 
 |-  F/_ j <_
19 nfcv 
 |-  F/_ j y
20 17 18 19 nfbr 
 |-  F/ j ( abs ` ( F ` x ) ) <_ y
21 13 20 nfim 
 |-  F/ j ( i <_ x -> ( abs ` ( F ` x ) ) <_ y )
22 breq2 
 |-  ( j = x -> ( i <_ j <-> i <_ x ) )
23 2fveq3 
 |-  ( j = x -> ( abs ` ( F ` j ) ) = ( abs ` ( F ` x ) ) )
24 23 breq1d 
 |-  ( j = x -> ( ( abs ` ( F ` j ) ) <_ y <-> ( abs ` ( F ` x ) ) <_ y ) )
25 22 24 imbi12d 
 |-  ( j = x -> ( ( i <_ j -> ( abs ` ( F ` j ) ) <_ y ) <-> ( i <_ x -> ( abs ` ( F ` x ) ) <_ y ) ) )
26 12 21 25 cbvralw 
 |-  ( A. j e. A ( i <_ j -> ( abs ` ( F ` j ) ) <_ y ) <-> A. x e. A ( i <_ x -> ( abs ` ( F ` x ) ) <_ y ) )
27 26 a1i 
 |-  ( k = i -> ( A. j e. A ( i <_ j -> ( abs ` ( F ` j ) ) <_ y ) <-> A. x e. A ( i <_ x -> ( abs ` ( F ` x ) ) <_ y ) ) )
28 11 27 bitrd 
 |-  ( k = i -> ( A. j e. A ( k <_ j -> ( abs ` ( F ` j ) ) <_ y ) <-> A. x e. A ( i <_ x -> ( abs ` ( F ` x ) ) <_ y ) ) )
29 8 28 cbvrex2vw 
 |-  ( E. b e. RR E. k e. RR A. j e. A ( k <_ j -> ( abs ` ( F ` j ) ) <_ b ) <-> E. y e. RR E. i e. RR A. x e. A ( i <_ x -> ( abs ` ( F ` x ) ) <_ y ) )
30 5 29 sylib 
 |-  ( ph -> E. y e. RR E. i e. RR A. x e. A ( i <_ x -> ( abs ` ( F ` x ) ) <_ y ) )
31 2 3 4 30 limsupre 
 |-  ( ph -> ( limsup ` F ) e. RR )