Theorem liminfltlimsupex

Description: An example where the liminf is strictly smaller than the limsup . (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step	Hyp	Ref	Expression
1		liminfltlimsupex.1	$$⊢F=\left(n\in \mathbb{N}⟼if\left(2\parallel n,0,1\right)\right)$$
2		0lt1	$$⊢0<1$$
3	1	liminf10ex	$$⊢\mathrm{lim\; inf}\left(F\right)=0$$
4	1	limsup10ex	$$⊢\mathrm{lim\; sup}\left(F\right)=1$$
5	3 4	breq12i	$$⊢\mathrm{lim\; inf}\left(F\right)<\mathrm{lim\; sup}\left(F\right)\leftrightarrow 0<1$$
6	2 5	mpbir	$$⊢\mathrm{lim\; inf}\left(F\right)<\mathrm{lim\; sup}\left(F\right)$$