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

Metamath Proof Explorer

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 ..^N) \subseteq ℕ$

Step	Hyp	Ref	Expression
1		fzossfz	$⊢ (1 ..^N) \subseteq (1 \dots N)$
2		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
3	1 2	sstri	$⊢ (1 ..^N) \subseteq ℕ$