Theorem limsupref

Description: If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupref.j	$$⊢\underset{\_}{Ⅎ}jF$$
	limsupref.a	$$⊢\phi \to A\subseteq ℝ$$
	limsupref.s	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
	limsupref.f	$$⊢\phi \to F:A⟶ℝ$$
	limsupref.b	$$⊢\phi \to \exists b\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to \left|F\left(j\right)\right|\le b\right)$$
Assertion	limsupref	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		limsupref.j	$$⊢\underset{\_}{Ⅎ}jF$$
2		limsupref.a	$$⊢\phi \to A\subseteq ℝ$$
3		limsupref.s	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
4		limsupref.f	$$⊢\phi \to F:A⟶ℝ$$
5		limsupref.b	$$⊢\phi \to \exists b\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to \left|F\left(j\right)\right|\le b\right)$$
6		breq2	$$⊢b=y\to \left(\left|F\left(j\right)\right|\le b\leftrightarrow \left|F\left(j\right)\right|\le y\right)$$
7	6	imbi2d	$$⊢b=y\to \left(\left(k\le j\to \left|F\left(j\right)\right|\le b\right)\leftrightarrow \left(k\le j\to \left|F\left(j\right)\right|\le y\right)\right)$$
8	7	ralbidv	$$⊢b=y\to \left(\forall j\in A\left(k\le j\to \left|F\left(j\right)\right|\le b\right)\leftrightarrow \forall j\in A\left(k\le j\to \left|F\left(j\right)\right|\le y\right)\right)$$
9		breq1	$$⊢k=i\to \left(k\le j\leftrightarrow i\le j\right)$$
10	9	imbi1d	$$⊢k=i\to \left(\left(k\le j\to \left|F\left(j\right)\right|\le y\right)\leftrightarrow \left(i\le j\to \left|F\left(j\right)\right|\le y\right)\right)$$
11	10	ralbidv	$$⊢k=i\to \left(\forall j\in A\left(k\le j\to \left|F\left(j\right)\right|\le y\right)\leftrightarrow \forall j\in A\left(i\le j\to \left|F\left(j\right)\right|\le y\right)\right)$$
12		nfv	$$⊢Ⅎx\left(i\le j\to \left|F\left(j\right)\right|\le y\right)$$
13		nfv	$$⊢Ⅎji\le x$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}j\mathrm{abs}$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}jx$$
16	1 15	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(x\right)$$
17	14 16	nffv	$$⊢\underset{\_}{Ⅎ}j\left|F\left(x\right)\right|$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}j\le$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}jy$$
20	17 18 19	nfbr	$$⊢Ⅎj\left|F\left(x\right)\right|\le y$$
21	13 20	nfim	$$⊢Ⅎj\left(i\le x\to \left|F\left(x\right)\right|\le y\right)$$
22		breq2	$$⊢j=x\to \left(i\le j\leftrightarrow i\le x\right)$$
23		2fveq3	$$⊢j=x\to \left|F\left(j\right)\right|=\left|F\left(x\right)\right|$$
24	23	breq1d	$$⊢j=x\to \left(\left|F\left(j\right)\right|\le y\leftrightarrow \left|F\left(x\right)\right|\le y\right)$$
25	22 24	imbi12d	$$⊢j=x\to \left(\left(i\le j\to \left|F\left(j\right)\right|\le y\right)\leftrightarrow \left(i\le x\to \left|F\left(x\right)\right|\le y\right)\right)$$
26	12 21 25	cbvralw	$$⊢\forall j\in A\left(i\le j\to \left|F\left(j\right)\right|\le y\right)\leftrightarrow \forall x\in A\left(i\le x\to \left|F\left(x\right)\right|\le y\right)$$
27	26	a1i	$$⊢k=i\to \left(\forall j\in A\left(i\le j\to \left|F\left(j\right)\right|\le y\right)\leftrightarrow \forall x\in A\left(i\le x\to \left|F\left(x\right)\right|\le y\right)\right)$$
28	11 27	bitrd	$$⊢k=i\to \left(\forall j\in A\left(k\le j\to \left|F\left(j\right)\right|\le y\right)\leftrightarrow \forall x\in A\left(i\le x\to \left|F\left(x\right)\right|\le y\right)\right)$$
29	8 28	cbvrex2vw	$$⊢\exists b\in ℝ\exists k\in ℝ\forall j\in A\left(k\le j\to \left|F\left(j\right)\right|\le b\right)\leftrightarrow \exists y\in ℝ\exists i\in ℝ\forall x\in A\left(i\le x\to \left|F\left(x\right)\right|\le y\right)$$
30	5 29	sylib	$$⊢\phi \to \exists y\in ℝ\exists i\in ℝ\forall x\in A\left(i\le x\to \left|F\left(x\right)\right|\le y\right)$$
31	2 3 4 30	limsupre	$$⊢\phi \to \mathrm{lim\; sup}\left(F\right)\in ℝ$$