Theorem fzssnn0

Description: A finite set of sequential integers that is a subset of NN0 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Assertion	fzssnn0	$$⊢\left(0\dots N\right)\subseteq {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		fzssuz	$$⊢\left(0\dots N\right)\subseteq {\mathbb{Z}}_{\ge 0}$$
2		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
3	2	eqcomi	$$⊢{\mathbb{Z}}_{\ge 0}={\mathbb{N}}_0$$
4	1 3	sseqtri	$$⊢\left(0\dots N\right)\subseteq {\mathbb{N}}_0$$