Theorem liminfpnfuz

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

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

Proof

Step	Hyp	Ref	Expression
1		liminfpnfuz.1	$$⊢\underset{\_}{Ⅎ}jF$$
2		liminfpnfuz.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		liminfpnfuz.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		liminfpnfuz.4	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
5		nfv	$$⊢Ⅎl\phi$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}lF$$
7	5 6 2 3 4	liminfvaluz3	$$⊢\phi \to \mathrm{lim\; inf}\left(F\right)=-\mathrm{lim\; sup}\left(\left(l\in Z⟼-F\left(l\right)\right)\right)$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}jl$$
9	1 8	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(l\right)$$
10	9	nfxneg	$$⊢\underset{\_}{Ⅎ}j\left(-F\left(l\right)\right)$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}l\left(-F\left(j\right)\right)$$
12		fveq2	$$⊢l=j\to F\left(l\right)=F\left(j\right)$$
13	12	xnegeqd	$$⊢l=j\to -F\left(l\right)=-F\left(j\right)$$
14	10 11 13	cbvmpt	$$⊢\left(l\in Z⟼-F\left(l\right)\right)=\left(j\in Z⟼-F\left(j\right)\right)$$
15	14	fveq2i	$$⊢\mathrm{lim\; sup}\left(\left(l\in Z⟼-F\left(l\right)\right)\right)=\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)$$
16	15	xnegeqi	$$⊢-\mathrm{lim\; sup}\left(\left(l\in Z⟼-F\left(l\right)\right)\right)=-\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)$$
17	7 16	eqtrdi	$$⊢\phi \to \mathrm{lim\; inf}\left(F\right)=-\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)$$
18	17	eqeq1d	$$⊢\phi \to \left(\mathrm{lim\; inf}\left(F\right)=\mathrm{+\infty }\leftrightarrow -\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)=\mathrm{+\infty }\right)$$
19		xnegmnf	$$⊢-\mathrm{-\infty }=\mathrm{+\infty }$$
20	19	eqcomi	$$⊢\mathrm{+\infty }=-\mathrm{-\infty }$$
21	20	a1i	$$⊢\phi \to \mathrm{+\infty }=-\mathrm{-\infty }$$
22	21	eqeq2d	$$⊢\phi \to \left(-\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)=\mathrm{+\infty }\leftrightarrow -\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)=-\mathrm{-\infty }\right)$$
23	3	fvexi	$$⊢Z\in \mathrm{V}$$
24	23	mptex	$$⊢\left(j\in Z⟼-F\left(j\right)\right)\in \mathrm{V}$$
25	24	a1i	$$⊢\phi \to \left(j\in Z⟼-F\left(j\right)\right)\in \mathrm{V}$$
26	25	limsupcld	$$⊢\phi \to \mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)\in {ℝ}^{*}$$
27		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
28		xneg11	$$⊢\left(\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)\in {ℝ}^{*}\wedge \mathrm{-\infty }\in {ℝ}^{*}\right)\to \left(-\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)=-\mathrm{-\infty }\leftrightarrow \mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)=\mathrm{-\infty }\right)$$
29	26 27 28	sylancl	$$⊢\phi \to \left(-\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)=-\mathrm{-\infty }\leftrightarrow \mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)=\mathrm{-\infty }\right)$$
30	22 29	bitrd	$$⊢\phi \to \left(-\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)=\mathrm{+\infty }\leftrightarrow \mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)=\mathrm{-\infty }\right)$$
31	3	uztrn2	$$⊢\left(k\in Z\wedge j\in {\mathbb{Z}}_{\ge k}\right)\to j\in Z$$
32		xnegex	$$⊢-F\left(j\right)\in \mathrm{V}$$
33		fvmpt4	$$⊢\left(j\in Z\wedge -F\left(j\right)\in \mathrm{V}\right)\to \left(j\in Z⟼-F\left(j\right)\right)\left(j\right)=-F\left(j\right)$$
34	31 32 33	sylancl	$$⊢\left(k\in Z\wedge j\in {\mathbb{Z}}_{\ge k}\right)\to \left(j\in Z⟼-F\left(j\right)\right)\left(j\right)=-F\left(j\right)$$
35	34	breq1d	$$⊢\left(k\in Z\wedge j\in {\mathbb{Z}}_{\ge k}\right)\to \left(\left(j\in Z⟼-F\left(j\right)\right)\left(j\right)\le x\leftrightarrow -F\left(j\right)\le x\right)$$
36	35	ralbidva	$$⊢k\in Z\to \left(\forall j\in {\mathbb{Z}}_{\ge k}\left(j\in Z⟼-F\left(j\right)\right)\left(j\right)\le x\leftrightarrow \forall j\in {\mathbb{Z}}_{\ge k}-F\left(j\right)\le x\right)$$
37	36	rexbiia	$$⊢\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}\left(j\in Z⟼-F\left(j\right)\right)\left(j\right)\le x\leftrightarrow \exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}-F\left(j\right)\le x$$
38	37	ralbii	$$⊢\forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}\left(j\in Z⟼-F\left(j\right)\right)\left(j\right)\le x\leftrightarrow \forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}-F\left(j\right)\le x$$
39	38	a1i	$$⊢\phi \to \left(\forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}\left(j\in Z⟼-F\left(j\right)\right)\left(j\right)\le x\leftrightarrow \forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}-F\left(j\right)\le x\right)$$
40		nfmpt1	$$⊢\underset{\_}{Ⅎ}j\left(j\in Z⟼-F\left(j\right)\right)$$
41	4	ffvelrnda	$$⊢\left(\phi \wedge l\in Z\right)\to F\left(l\right)\in {ℝ}^{*}$$
42	41	xnegcld	$$⊢\left(\phi \wedge l\in Z\right)\to -F\left(l\right)\in {ℝ}^{*}$$
43	14	eqcomi	$$⊢\left(j\in Z⟼-F\left(j\right)\right)=\left(l\in Z⟼-F\left(l\right)\right)$$
44	42 43	fmptd	$$⊢\phi \to \left(j\in Z⟼-F\left(j\right)\right):Z⟶{ℝ}^{*}$$
45	40 2 3 44	limsupmnfuz	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)=\mathrm{-\infty }\leftrightarrow \forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}\left(j\in Z⟼-F\left(j\right)\right)\left(j\right)\le x\right)$$
46	1 3 4	xlimpnfxnegmnf	$$⊢\phi \to \left(\forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\leftrightarrow \forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}-F\left(j\right)\le x\right)$$
47	39 45 46	3bitr4d	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(\left(j\in Z⟼-F\left(j\right)\right)\right)=\mathrm{-\infty }\leftrightarrow \forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$
48	18 30 47	3bitrd	$$⊢\phi \to \left(\mathrm{lim\; inf}\left(F\right)=\mathrm{+\infty }\leftrightarrow \forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}x\le F\left(j\right)\right)$$