Theorem fzossnn0

Description: A half-open integer range starting at a nonnegative integer is a subset of the nonnegative integers. (Contributed by Alexander van der Vekens, 13-May-2018)

	Ref	Expression
Assertion	fzossnn0	$$⊢M\in {\mathbb{N}}_0\to \left(M..^N\right)\subseteq {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		fzossfz	$$⊢\left(M..^N\right)\subseteq \left(M\dots N\right)$$
2		fzss1	$$⊢M\in {\mathbb{Z}}_{\ge 0}\to \left(M\dots N\right)\subseteq \left(0\dots N\right)$$
3		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
4	2 3	eleq2s	$$⊢M\in {\mathbb{N}}_0\to \left(M\dots N\right)\subseteq \left(0\dots N\right)$$
5	1 4	sstrid	$$⊢M\in {\mathbb{N}}_0\to \left(M..^N\right)\subseteq \left(0\dots N\right)$$
6		fz0ssnn0	$$⊢\left(0\dots N\right)\subseteq {\mathbb{N}}_0$$
7	5 6	sstrdi	$$⊢M\in {\mathbb{N}}_0\to \left(M..^N\right)\subseteq {\mathbb{N}}_0$$