Theorem fz0ssnn0

Description: Finite sets of sequential nonnegative integers starting with 0 are subsets of NN0. (Contributed by JJ, 1-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		elfznn0	$$⊢k\in \left(0\dots N\right)\to k\in {\mathbb{N}}_0$$
2	1	ssriv	$$⊢\left(0\dots N\right)\subseteq {\mathbb{N}}_0$$