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	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		elfzelz	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℤ )
2		elfzle1	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 1 ≤ 𝐾 )
3		elnnz1	⊢ ( 𝐾 ∈ ℕ ↔ ( 𝐾 ∈ ℤ ∧ 1 ≤ 𝐾 ) )
4	1 2 3	sylanbrc	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℕ )