Theorem limsup10ex

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

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

Proof

Step	Hyp	Ref	Expression
1		limsup10ex.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	limsupval3	$$⊢\top \to \mathrm{lim\; sup}\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\; sup}\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	supeq1d	$$⊢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		suppr	$$⊢\left(<\mathrm{Or}{ℝ}^{*}\wedge 0\in {ℝ}^{*}\wedge 1\in {ℝ}^{*}\right)\to sup\left(\left\{0,1\right\},{ℝ}^{*},<\right)=if\left(1<0,0,1\right)$$
20	18 5 7 19	mp3an	$$⊢sup\left(\left\{0,1\right\},{ℝ}^{*},<\right)=if\left(1<0,0,1\right)$$
21		0le1	$$⊢0\le 1$$
22		0re	$$⊢0\in ℝ$$
23		1re	$$⊢1\in ℝ$$
24	22 23	lenlti	$$⊢0\le 1\leftrightarrow \neg 1<0$$
25	21 24	mpbi	$$⊢\neg 1<0$$
26	25	iffalsei	$$⊢if\left(1<0,0,1\right)=1$$
27	20 26	eqtri	$$⊢sup\left(\left\{0,1\right\},{ℝ}^{*},<\right)=1$$
28	17 27	eqtrdi	$$⊢k\in ℝ\to sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)=1$$
29	28	mpteq2ia	$$⊢\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)=\left(k\in ℝ⟼1\right)$$
30	29	rneqi	$$⊢\mathrm{ran}\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)=\mathrm{ran}\left(k\in ℝ⟼1\right)$$
31		eqid	$$⊢\left(k\in ℝ⟼1\right)=\left(k\in ℝ⟼1\right)$$
32		ren0	$$⊢ℝ\ne \varnothing$$
33	32	a1i	$$⊢\top \to ℝ\ne \varnothing$$
34	31 33	rnmptc	$$⊢\top \to \mathrm{ran}\left(k\in ℝ⟼1\right)=\left\{1\right\}$$
35	34	mptru	$$⊢\mathrm{ran}\left(k\in ℝ⟼1\right)=\left\{1\right\}$$
36	30 35	eqtri	$$⊢\mathrm{ran}\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right)=\left\{1\right\}$$
37	36	infeq1i	$$⊢sup\left(\mathrm{ran}\left(k\in ℝ⟼sup\left(F\left[\left[k,\mathrm{+\infty }\right)\right],{ℝ}^{*},<\right)\right),{ℝ}^{*},<\right)=sup\left(\left\{1\right\},{ℝ}^{*},<\right)$$
38		infsn	$$⊢\left(<\mathrm{Or}{ℝ}^{*}\wedge 1\in {ℝ}^{*}\right)\to sup\left(\left\{1\right\},{ℝ}^{*},<\right)=1$$
39	18 7 38	mp2an	$$⊢sup\left(\left\{1\right\},{ℝ}^{*},<\right)=1$$
40	14 37 39	3eqtri	$$⊢\mathrm{lim\; sup}\left(F\right)=1$$