Theorem elfz2nn

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

	Ref	Expression
Assertion	elfz2nn	$$⊢K\in \left(2\dots N\right)\to K\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		2eluzge1	$$⊢2\in {\mathbb{Z}}_{\ge 1}$$
2		fzss1	$$⊢2\in {\mathbb{Z}}_{\ge 1}\to \left(2\dots N\right)\subseteq \left(1\dots N\right)$$
3	1 2	ax-mp	$$⊢\left(2\dots N\right)\subseteq \left(1\dots N\right)$$
4	3	sseli	$$⊢K\in \left(2\dots N\right)\to K\in \left(1\dots N\right)$$
5		elfznn	$$⊢K\in \left(1\dots N\right)\to K\in \mathbb{N}$$
6	4 5	syl	$$⊢K\in \left(2\dots N\right)\to K\in \mathbb{N}$$