Theorem fzssnn

Description: Finite sets of sequential integers starting from a natural are a subset of the positive integers. (Contributed by Thierry Arnoux, 4-Aug-2017)

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

Proof

Step	Hyp	Ref	Expression
1		fzss1	$$⊢M\in {\mathbb{Z}}_{\ge 1}\to \left(M\dots N\right)\subseteq \left(1\dots N\right)$$
2		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
3	1 2	eleq2s	$$⊢M\in \mathbb{N}\to \left(M\dots N\right)\subseteq \left(1\dots N\right)$$
4		fz1ssnn	$$⊢\left(1\dots N\right)\subseteq \mathbb{N}$$
5	3 4	sstrdi	$$⊢M\in \mathbb{N}\to \left(M\dots N\right)\subseteq \mathbb{N}$$