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

Proof

Step	Hyp	Ref	Expression
1		fzssuz	⊢ ( 0 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 0 )
2		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
3	2	eqcomi	⊢ ( ℤ≥ ‘ 0 ) = ℕ0
4	1 3	sseqtri	⊢ ( 0 ... 𝑁 ) ⊆ ℕ0