Theorem fz2ssnn0

Description: A finite set of sequential integers that is a subset of NN0 . (Contributed by Thierry Arnoux, 8-Dec-2021)

	Ref	Expression
Assertion	fz2ssnn0	$$⊢M\in {\mathbb{N}}_0\to \left(M\dots N\right)\subseteq {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		fzssuz	$$⊢\left(M\dots N\right)\subseteq {\mathbb{Z}}_{\ge M}$$
2		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
3	2	eleq2i	$$⊢M\in {\mathbb{N}}_0\leftrightarrow M\in {\mathbb{Z}}_{\ge 0}$$
4	3	biimpi	$$⊢M\in {\mathbb{N}}_0\to M\in {\mathbb{Z}}_{\ge 0}$$
5		uzss	$$⊢M\in {\mathbb{Z}}_{\ge 0}\to {\mathbb{Z}}_{\ge M}\subseteq {\mathbb{Z}}_{\ge 0}$$
6	4 5	syl	$$⊢M\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\ge M}\subseteq {\mathbb{Z}}_{\ge 0}$$
7	6 2	sseqtrrdi	$$⊢M\in {\mathbb{N}}_0\to {\mathbb{Z}}_{\ge M}\subseteq {\mathbb{N}}_0$$
8	1 7	sstrid	$$⊢M\in {\mathbb{N}}_0\to \left(M\dots N\right)\subseteq {\mathbb{N}}_0$$