Metamath Proof Explorer

Theorem elfzo2nn

Description: A member of a half-open range of integers starting at 2 is a positive integer. (Contributed by AV, 5-Apr-2026)

		Ref	Expression
	Assertion	elfzo2nn	$⊢ K \in (2 ..^N) \to K \in ℕ$

Step	Hyp	Ref	Expression
1		elfzo2	$⊢ K \in (2 ..^N) \leftrightarrow (K \in ℤ_{\geq 2} \land N \in ℤ \land K < N)$
2		eluz2nn	$⊢ K \in ℤ_{\geq 2} \to K \in ℕ$
3	2	3ad2ant1	$⊢ (K \in ℤ_{\geq 2} \land N \in ℤ \land K < N) \to K \in ℕ$
4	1 3	sylbi	$⊢ K \in (2 ..^N) \to K \in ℕ$