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

Metamath Proof Explorer

Theorem elfzonn0

Description: A member of a half-open range of nonnegative integers is a nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018)

		Ref	Expression
	Assertion	elfzonn0	$⊢ K \in (0 ..^N) \to K \in ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		elfzouz	$⊢ K \in (0 ..^N) \to K \in ℤ_{\geq 0}$
2		elnn0uz	$⊢ K \in ℕ_{0} \leftrightarrow K \in ℤ_{\geq 0}$
3	1 2	sylibr	$⊢ K \in (0 ..^N) \to K \in ℕ_{0}$