Theorem limsupmnfuz

Description: The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		limsupmnfuz.1	$$⊢\underset{\_}{Ⅎ}jF$$
2		limsupmnfuz.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		limsupmnfuz.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		limsupmnfuz.4	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
5	2 3 4	limsupmnfuzlem	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)=\mathrm{-\infty }\leftrightarrow \forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\right)$$
6		breq2	$$⊢y=x\to \left(F\left(l\right)\le y\leftrightarrow F\left(l\right)\le x\right)$$
7	6	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)$$
8	7	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)$$
9		fveq2	$$⊢i=k\to {\mathbb{Z}}_{\ge i}={\mathbb{Z}}_{\ge k}$$
10	9	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)$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}jl$$
12	1 11	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(l\right)$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}j\le$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}jx$$
15	12 13 14	nfbr	$$⊢ℲjF\left(l\right)\le x$$
16		nfv	$$⊢ℲlF\left(j\right)\le x$$
17		fveq2	$$⊢l=j\to F\left(l\right)=F\left(j\right)$$
18	17	breq1d	$$⊢l=j\to \left(F\left(l\right)\le x\leftrightarrow F\left(j\right)\le x\right)$$
19	15 16 18	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$$
20	19	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)$$
21	10 20	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)$$
22	21	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$$
23	22	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)$$
24	8 23	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)$$
25	24	cbvralvw	$$⊢\forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x$$
26	25	a1i	$$⊢\phi \to \left(\forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
27	5 26	bitrd	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)=\mathrm{-\infty }\leftrightarrow \forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$