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 ..^ 𝑁 ) ⊆ ℕ0

Proof

Step	Hyp	Ref	Expression
1		elfzonn0	⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → 𝑘 ∈ ℕ0 )
2	1	ssriv	⊢ ( 0 ..^ 𝑁 ) ⊆ ℕ0