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

Proof

Step	Hyp	Ref	Expression
1		elfzo2	⊢ ( 𝐾 ∈ ( 2 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
2		eluz2nn	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℕ )
3	2	3ad2ant1	⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) → 𝐾 ∈ ℕ )
4	1 3	sylbi	⊢ ( 𝐾 ∈ ( 2 ..^ 𝑁 ) → 𝐾 ∈ ℕ )