Theorem limsupre3uz

Description: Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, infinitely often; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupre3uz.1	$$⊢\underset{\_}{Ⅎ}jF$$
	limsupre3uz.2	$$⊢\phi \to M\in \mathbb{Z}$$
	limsupre3uz.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	limsupre3uz.4	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
Assertion	limsupre3uz	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\wedge \exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		limsupre3uz.1	$$⊢\underset{\_}{Ⅎ}jF$$
2		limsupre3uz.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		limsupre3uz.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		limsupre3uz.4	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}lF$$
6	5 2 3 4	limsupre3uzlem	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\exists y\in ℝ\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\wedge \exists y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\right)\right)$$
7		breq1	$$⊢y=x\to \left(y\le F\left(l\right)\leftrightarrow x\le F\left(l\right)\right)$$
8	7	rexbidv	$$⊢y=x\to \left(\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\right)$$
9	8	ralbidv	$$⊢y=x\to \left(\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\right)$$
10		fveq2	$$⊢i=k\to {\mathbb{Z}}_{\ge i}={\mathbb{Z}}_{\ge k}$$
11	10	rexeqdv	$$⊢i=k\to \left(\exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \exists l\in {\mathbb{Z}}_{\ge k}x\le F\left(l\right)\right)$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}jx$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}j\le$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}jl$$
15	1 14	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(l\right)$$
16	12 13 15	nfbr	$$⊢Ⅎjx\le F\left(l\right)$$
17		nfv	$$⊢Ⅎlx\le F\left(j\right)$$
18		fveq2	$$⊢l=j\to F\left(l\right)=F\left(j\right)$$
19	18	breq2d	$$⊢l=j\to \left(x\le F\left(l\right)\leftrightarrow x\le F\left(j\right)\right)$$
20	16 17 19	cbvrexw	$$⊢\exists l\in {\mathbb{Z}}_{\ge k}x\le F\left(l\right)\leftrightarrow \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
21	20	a1i	$$⊢i=k\to \left(\exists l\in {\mathbb{Z}}_{\ge k}x\le F\left(l\right)\leftrightarrow \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
22	11 21	bitrd	$$⊢i=k\to \left(\exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
23	22	cbvralvw	$$⊢\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
24	23	a1i	$$⊢y=x\to \left(\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
25	9 24	bitrd	$$⊢y=x\to \left(\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
26	25	cbvrexvw	$$⊢\exists y\in ℝ\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)$$
27		breq2	$$⊢y=x\to \left(F\left(l\right)\le y\leftrightarrow F\left(l\right)\le x\right)$$
28	27	ralbidv	$$⊢y=x\to \left(\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\right)$$
29	28	rexbidv	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\right)$$
30	10	raleqdv	$$⊢i=k\to \left(\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \forall l\in {\mathbb{Z}}_{\ge k}F\left(l\right)\le x\right)$$
31	15 13 12	nfbr	$$⊢ℲjF\left(l\right)\le x$$
32		nfv	$$⊢ℲlF\left(j\right)\le x$$
33	18	breq1d	$$⊢l=j\to \left(F\left(l\right)\le x\leftrightarrow F\left(j\right)\le x\right)$$
34	31 32 33	cbvralw	$$⊢\forall l\in {\mathbb{Z}}_{\ge k}F\left(l\right)\le x\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x$$
35	34	a1i	$$⊢i=k\to \left(\forall l\in {\mathbb{Z}}_{\ge k}F\left(l\right)\le x\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
36	30 35	bitrd	$$⊢i=k\to \left(\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
37	36	cbvrexvw	$$⊢\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x$$
38	37	a1i	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
39	29 38	bitrd	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
40	39	cbvrexvw	$$⊢\exists y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x$$
41	26 40	anbi12i	$$⊢\left(\exists y\in ℝ\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\wedge \exists y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\right)\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\wedge \exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
42	41	a1i	$$⊢\phi \to \left(\left(\exists y\in ℝ\forall i\in Z\exists l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\wedge \exists y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\right)\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\wedge \exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\right)$$
43	6 42	bitrd	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\in ℝ\leftrightarrow \left(\exists x\in ℝ\forall k\in Z\exists j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\wedge \exists x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)\right)$$