Theorem liminfreuz

Description: Given a function on the reals, its inferior limit is real if and only if two condition holds: 1. there is a real number that is greater than or equal to the function, infinitely often; 2. there is a real number that is smaller than or equal to the function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

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