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	$$⊢\underset{\_}{Ⅎ}kF$$
	liminflt.m	$$⊢\phi \to M\in \mathbb{Z}$$
	liminflt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	liminflt.f	$$⊢\phi \to F:Z⟶ℝ$$
	liminflt.r	$$⊢\phi \to \mathrm{lim\; inf}\left(F\right)\in ℝ$$
	liminflt.x	$$⊢\phi \to X\in {ℝ}^{+}$$
Assertion	liminflt	$$⊢\phi \to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\mathrm{lim\; inf}\left(F\right)<F\left(k\right)+X$$

Proof

Step	Hyp	Ref	Expression
1		liminflt.k	$$⊢\underset{\_}{Ⅎ}kF$$
2		liminflt.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		liminflt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		liminflt.f	$$⊢\phi \to F:Z⟶ℝ$$
5		liminflt.r	$$⊢\phi \to \mathrm{lim\; inf}\left(F\right)\in ℝ$$
6		liminflt.x	$$⊢\phi \to X\in {ℝ}^{+}$$
7	2 3 4 5 6	liminfltlem	$$⊢\phi \to \exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\mathrm{lim\; inf}\left(F\right)<F\left(l\right)+X$$
8		fveq2	$$⊢i=j\to {\mathbb{Z}}_{\ge i}={\mathbb{Z}}_{\ge j}$$
9	8	raleqdv	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}\mathrm{lim\; inf}\left(F\right)<F\left(l\right)+X\leftrightarrow \forall l\in {\mathbb{Z}}_{\ge j}\mathrm{lim\; inf}\left(F\right)<F\left(l\right)+X\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}k\mathrm{lim\; inf}$$
11	10 1	nffv	$$⊢\underset{\_}{Ⅎ}k\mathrm{lim\; inf}\left(F\right)$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}k<$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}kl$$
14	1 13	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(l\right)$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}k+$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}kX$$
17	14 15 16	nfov	$$⊢\underset{\_}{Ⅎ}k\left(F\left(l\right)+X\right)$$
18	11 12 17	nfbr	$$⊢Ⅎk\mathrm{lim\; inf}\left(F\right)<F\left(l\right)+X$$
19		nfv	$$⊢Ⅎl\mathrm{lim\; inf}\left(F\right)<F\left(k\right)+X$$
20		fveq2	$$⊢l=k\to F\left(l\right)=F\left(k\right)$$
21	20	oveq1d	$$⊢l=k\to F\left(l\right)+X=F\left(k\right)+X$$
22	21	breq2d	$$⊢l=k\to \left(\mathrm{lim\; inf}\left(F\right)<F\left(l\right)+X\leftrightarrow \mathrm{lim\; inf}\left(F\right)<F\left(k\right)+X\right)$$
23	18 19 22	cbvralw	$$⊢\forall l\in {\mathbb{Z}}_{\ge j}\mathrm{lim\; inf}\left(F\right)<F\left(l\right)+X\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}\mathrm{lim\; inf}\left(F\right)<F\left(k\right)+X$$
24	23	a1i	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge j}\mathrm{lim\; inf}\left(F\right)<F\left(l\right)+X\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}\mathrm{lim\; inf}\left(F\right)<F\left(k\right)+X\right)$$
25	9 24	bitrd	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}\mathrm{lim\; inf}\left(F\right)<F\left(l\right)+X\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}\mathrm{lim\; inf}\left(F\right)<F\left(k\right)+X\right)$$
26	25	cbvrexvw	$$⊢\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\mathrm{lim\; inf}\left(F\right)<F\left(l\right)+X\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\mathrm{lim\; inf}\left(F\right)<F\left(k\right)+X$$
27	7 26	sylib	$$⊢\phi \to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\mathrm{lim\; inf}\left(F\right)<F\left(k\right)+X$$