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

Metamath Proof Explorer

Theorem elfz3nn0

Description: The upper bound of a nonempty finite set of sequential nonnegative integers is a nonnegative integer. (Contributed by NM, 16-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	elfz3nn0	$⊢ K \in (0 \dots N) \to N \in ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		elfz2nn0	$⊢ K \in (0 \dots N) \leftrightarrow (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N)$
2	1	simp2bi	$⊢ K \in (0 \dots N) \to N \in ℕ_{0}$