Theorem limsuppnf

Description: If the restriction of a function to every upper interval is unbounded above, its limsup is +oo . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		limsuppnf.j	$$⊢\underset{\_}{Ⅎ}jF$$
2		limsuppnf.a	$$⊢\phi \to A\subseteq ℝ$$
3		limsuppnf.f	$$⊢\phi \to F:A⟶{ℝ}^{*}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}lF$$
5	4 2 3	limsuppnflem	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)=\mathrm{+\infty }\leftrightarrow \forall y\in ℝ\forall i\in ℝ\exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)\right)$$
6		breq1	$$⊢i=k\to \left(i\le l\leftrightarrow k\le l\right)$$
7	6	anbi1d	$$⊢i=k\to \left(\left(i\le l\wedge y\le F\left(l\right)\right)\leftrightarrow \left(k\le l\wedge y\le F\left(l\right)\right)\right)$$
8	7	rexbidv	$$⊢i=k\to \left(\exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)\leftrightarrow \exists l\in A\left(k\le l\wedge y\le F\left(l\right)\right)\right)$$
9		nfv	$$⊢Ⅎjk\le l$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}jy$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}j\le$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}jl$$
13	1 12	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(l\right)$$
14	10 11 13	nfbr	$$⊢Ⅎjy\le F\left(l\right)$$
15	9 14	nfan	$$⊢Ⅎj\left(k\le l\wedge y\le F\left(l\right)\right)$$
16		nfv	$$⊢Ⅎl\left(k\le j\wedge y\le F\left(j\right)\right)$$
17		breq2	$$⊢l=j\to \left(k\le l\leftrightarrow k\le j\right)$$
18		fveq2	$$⊢l=j\to F\left(l\right)=F\left(j\right)$$
19	18	breq2d	$$⊢l=j\to \left(y\le F\left(l\right)\leftrightarrow y\le F\left(j\right)\right)$$
20	17 19	anbi12d	$$⊢l=j\to \left(\left(k\le l\wedge y\le F\left(l\right)\right)\leftrightarrow \left(k\le j\wedge y\le F\left(j\right)\right)\right)$$
21	15 16 20	cbvrexw	$$⊢\exists l\in A\left(k\le l\wedge y\le F\left(l\right)\right)\leftrightarrow \exists j\in A\left(k\le j\wedge y\le F\left(j\right)\right)$$
22	21	a1i	$$⊢i=k\to \left(\exists l\in A\left(k\le l\wedge y\le F\left(l\right)\right)\leftrightarrow \exists j\in A\left(k\le j\wedge y\le F\left(j\right)\right)\right)$$
23	8 22	bitrd	$$⊢i=k\to \left(\exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)\leftrightarrow \exists j\in A\left(k\le j\wedge y\le F\left(j\right)\right)\right)$$
24	23	cbvralvw	$$⊢\forall i\in ℝ\exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)\leftrightarrow \forall k\in ℝ\exists j\in A\left(k\le j\wedge y\le F\left(j\right)\right)$$
25	24	a1i	$$⊢y=x\to \left(\forall i\in ℝ\exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)\leftrightarrow \forall k\in ℝ\exists j\in A\left(k\le j\wedge y\le F\left(j\right)\right)\right)$$
26		breq1	$$⊢y=x\to \left(y\le F\left(j\right)\leftrightarrow x\le F\left(j\right)\right)$$
27	26	anbi2d	$$⊢y=x\to \left(\left(k\le j\wedge y\le F\left(j\right)\right)\leftrightarrow \left(k\le j\wedge x\le F\left(j\right)\right)\right)$$
28	27	rexbidv	$$⊢y=x\to \left(\exists j\in A\left(k\le j\wedge y\le F\left(j\right)\right)\leftrightarrow \exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\right)$$
29	28	ralbidv	$$⊢y=x\to \left(\forall k\in ℝ\exists j\in A\left(k\le j\wedge y\le F\left(j\right)\right)\leftrightarrow \forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\right)$$
30	25 29	bitrd	$$⊢y=x\to \left(\forall i\in ℝ\exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)\leftrightarrow \forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\right)$$
31	30	cbvralvw	$$⊢\forall y\in ℝ\forall i\in ℝ\exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)\leftrightarrow \forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)$$
32	31	a1i	$$⊢\phi \to \left(\forall y\in ℝ\forall i\in ℝ\exists l\in A\left(i\le l\wedge y\le F\left(l\right)\right)\leftrightarrow \forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\right)$$
33	5 32	bitrd	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)=\mathrm{+\infty }\leftrightarrow \forall x\in ℝ\forall k\in ℝ\exists j\in A\left(k\le j\wedge x\le F\left(j\right)\right)\right)$$