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

Proof

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