Metamath Proof Explorer

Theorem limsupgt

Description: Given a sequence of real numbers, there exists an upper part of the sequence that's appxoximated from below by the superior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses limsupgt.k 
|- F/_ k F
limsupgt.m 
|- ( ph -> M e. ZZ )
limsupgt.z 
|- Z = ( ZZ>= ` M )
limsupgt.f 
|- ( ph -> F : Z --> RR )
limsupgt.r 
|- ( ph -> ( limsup ` F ) e. RR )
limsupgt.x 
|- ( ph -> X e. RR+ )
Assertion limsupgt 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - X ) < ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 limsupgt.k 
 |-  F/_ k F
2 limsupgt.m 
 |-  ( ph -> M e. ZZ )
3 limsupgt.z 
 |-  Z = ( ZZ>= ` M )
4 limsupgt.f 
 |-  ( ph -> F : Z --> RR )
5 limsupgt.r 
 |-  ( ph -> ( limsup ` F ) e. RR )
6 limsupgt.x 
 |-  ( ph -> X e. RR+ )
7 2 3 4 5 6 limsupgtlem 
 |-  ( ph -> E. i e. Z A. l e. ( ZZ>= ` i ) ( ( F ` l ) - X ) < ( limsup ` F ) )
8 nfcv 
 |-  F/_ k l
9 1 8 nffv 
 |-  F/_ k ( F ` l )
10 nfcv 
 |-  F/_ k -
11 nfcv 
 |-  F/_ k X
12 9 10 11 nfov 
 |-  F/_ k ( ( F ` l ) - X )
13 nfcv 
 |-  F/_ k <
14 nfcv 
 |-  F/_ k limsup
15 14 1 nffv 
 |-  F/_ k ( limsup ` F )
16 12 13 15 nfbr 
 |-  F/ k ( ( F ` l ) - X ) < ( limsup ` F )
17 nfv 
 |-  F/ l ( ( F ` k ) - X ) < ( limsup ` F )
18 fveq2 
 |-  ( l = k -> ( F ` l ) = ( F ` k ) )
19 18 oveq1d 
 |-  ( l = k -> ( ( F ` l ) - X ) = ( ( F ` k ) - X ) )
20 19 breq1d 
 |-  ( l = k -> ( ( ( F ` l ) - X ) < ( limsup ` F ) <-> ( ( F ` k ) - X ) < ( limsup ` F ) ) )
21 16 17 20 cbvralw 
 |-  ( A. l e. ( ZZ>= ` i ) ( ( F ` l ) - X ) < ( limsup ` F ) <-> A. k e. ( ZZ>= ` i ) ( ( F ` k ) - X ) < ( limsup ` F ) )
22 21 a1i 
 |-  ( i = j -> ( A. l e. ( ZZ>= ` i ) ( ( F ` l ) - X ) < ( limsup ` F ) <-> A. k e. ( ZZ>= ` i ) ( ( F ` k ) - X ) < ( limsup ` F ) ) )
23 fveq2 
 |-  ( i = j -> ( ZZ>= ` i ) = ( ZZ>= ` j ) )
24 23 raleqdv 
 |-  ( i = j -> ( A. k e. ( ZZ>= ` i ) ( ( F ` k ) - X ) < ( limsup ` F ) <-> A. k e. ( ZZ>= ` j ) ( ( F ` k ) - X ) < ( limsup ` F ) ) )
25 22 24 bitrd 
 |-  ( i = j -> ( A. l e. ( ZZ>= ` i ) ( ( F ` l ) - X ) < ( limsup ` F ) <-> A. k e. ( ZZ>= ` j ) ( ( F ` k ) - X ) < ( limsup ` F ) ) )
26 25 cbvrexvw 
 |-  ( E. i e. Z A. l e. ( ZZ>= ` i ) ( ( F ` l ) - X ) < ( limsup ` F ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - X ) < ( limsup ` F ) )
27 7 26 sylib 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) - X ) < ( limsup ` F ) )