Theorem fzo0ssnn0

Description: Half-open integer ranges starting with 0 are subsets of NN0. (Contributed by Thierry Arnoux, 8-Oct-2018) (Proof shortened by JJ, 1-Jun-2021)

	Ref	Expression
Assertion	fzo0ssnn0	$$⊢\left(0..^N\right)\subseteq {\mathbb{N}}_0$$

Proof

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