Theorem fzossnn

Description: Half-open integer ranges starting with 1 are subsets of NN. (Contributed by Thierry Arnoux, 28-Dec-2016)

	Ref	Expression
Assertion	fzossnn	⊢ ( 1 ..^ 𝑁 ) ⊆ ℕ

Proof

Step	Hyp	Ref	Expression
1		fzossfz	⊢ ( 1 ..^ 𝑁 ) ⊆ ( 1 ... 𝑁 )
2		fz1ssnn	⊢ ( 1 ... 𝑁 ) ⊆ ℕ
3	1 2	sstri	⊢ ( 1 ..^ 𝑁 ) ⊆ ℕ