This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem liminflt

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

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

Proof

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