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	$$⊢\left(1..^N\right)\subseteq \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		fzossfz	$$⊢\left(1..^N\right)\subseteq \left(1\dots N\right)$$
2		fz1ssnn	$$⊢\left(1\dots N\right)\subseteq \mathbb{N}$$
3	1 2	sstri	$$⊢\left(1..^N\right)\subseteq \mathbb{N}$$