Theorem liminf10ex

Description: The inferior limit of a function that alternates between two values. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypothesis	liminf10ex.1	$$⊢F=\left(n\in \mathbb{N}⟼if\left(2\parallel n,0,1\right)\right)$$
Assertion	liminf10ex	$$⊢\mathrm{lim\; inf}\left(F\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		liminf10ex.1	$$⊢F=\left(n\in \mathbb{N}⟼if\left(2\parallel n,0,1\right)\right)$$
2		nftru	$$⊢Ⅎk\top$$
3		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
4	3	a1i	$$⊢\top \to \mathbb{N}\in \mathrm{V}$$
5		0xr	$$⊢0\in {ℝ}^{*}$$
6	5	a1i	$$⊢n\in \mathbb{N}\to 0\in {ℝ}^{*}$$
7		1xr	$$⊢1\in {ℝ}^{*}$$
8	7	a1i	$$⊢n\in \mathbb{N}\to 1\in {ℝ}^{*}$$
9	6 8	ifcld	$$⊢n\in \mathbb{N}\to if\left(2\parallel n,0,1\right)\in {ℝ}^{*}$$
10	1 9	fmpti	$$⊢F:\mathbb{N}⟶{ℝ}^{*}$$
11	10	a1i	$$⊢\top \to F:\mathbb{N}⟶{ℝ}^{*}$$
12		eqid	$$⊢\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)=\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)$$
13	2 4 11 12	liminfval5	$$⊢\top \to \mathrm{lim\; inf}\left(F\right)=sup\left(\mathrm{ran}\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$$
14	13	mptru	$$⊢\mathrm{lim\; inf}\left(F\right)=sup\left(\mathrm{ran}\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)$$
15		id	$$⊢k\in ℝ\to k\in ℝ$$
16	1 15	limsup10exlem	$$⊢k\in ℝ\to F\left[\left[k,\mathrm{+\infty }\right)\right]=\left\{0,1\right\}$$
17	16	infeq1d	$$⊢k\in ℝ\to sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)=sup\left(\left\{0,1\right\},{ℝ}^{*},<\right)$$
18		xrltso	$$⊢<\mathrm{Or}{ℝ}^{*}$$
19		infpr	$$⊢\left(<\mathrm{Or}{ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\right)\to sup\left(\left\{0,1\right\},{ℝ}^{*},<\right)=if\left(0<1,0,1\right)$$
20	18 5 7 19	mp3an	$$⊢sup\left(\left\{0,1\right\},{ℝ}^{*},<\right)=if\left(0<1,0,1\right)$$
21		0lt1	$$⊢0<1$$
22	21	iftruei	$$⊢if\left(0<1,0,1\right)=0$$
23	20 22	eqtri	$$⊢sup\left(\left\{0,1\right\},{ℝ}^{*},<\right)=0$$
24	17 23	eqtrdi	$$⊢k\in ℝ\to sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)=0$$
25	24	mpteq2ia	$$⊢\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)=\left(k\in ℝ⟼0\right)$$
26	25	rneqi	$$⊢\mathrm{ran}\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)=\mathrm{ran}\left(k\in ℝ⟼0\right)$$
27		eqid	$$⊢\left(k\in ℝ⟼0\right)=\left(k\in ℝ⟼0\right)$$
28		ren0	$$⊢ℝ\ne \varnothing$$
29	28	a1i	$$⊢\top \to ℝ\ne \varnothing$$
30	27 29	rnmptc	$$⊢\top \to \mathrm{ran}\left(k\in ℝ⟼0\right)=\left\{0\right\}$$
31	30	mptru	$$⊢\mathrm{ran}\left(k\in ℝ⟼0\right)=\left\{0\right\}$$
32	26 31	eqtri	$$⊢\mathrm{ran}\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)=\left\{0\right\}$$
33	32	supeq1i	$$⊢sup\left(\mathrm{ran}\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)=sup\left(\left\{0\right\},{ℝ}^{*},<\right)$$
34		supsn	$$⊢\left(<\mathrm{Or}{ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$$
35	18 5 34	mp2an	$$⊢sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$$
36	14 33 35	3eqtri	$$⊢\mathrm{lim\; inf}\left(F\right)=0$$