This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (0 ..^N) \subseteq ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		elfzonn0	$⊢ k \in (0 ..^N) \to k \in ℕ_{0}$
2	1	ssriv	$⊢ (0 ..^N) \subseteq ℕ_{0}$