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 ) )

Metamath Proof Explorer

Theorem liminflt

Proof