Theorem elfznn

Description: A member of a finite set of sequential integers starting at 1 is a positive integer. (Contributed by NM, 24-Aug-2005)

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

Proof

Step	Hyp	Ref	Expression
1		elfzelz	$$⊢K\in \left(1\dots N\right)\to K\in \mathbb{Z}$$
2		elfzle1	$$⊢K\in \left(1\dots N\right)\to 1\le K$$
3		elnnz1	$$⊢K\in \mathbb{N}\leftrightarrow \left(K\in \mathbb{Z}\wedge 1\le K\right)$$
4	1 2 3	sylanbrc	$$⊢K\in \left(1\dots N\right)\to K\in \mathbb{N}$$