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 e. ( 2 ..^ N ) -> K e. NN )

Proof

Step Hyp Ref Expression
1 elfzo2 
 |-  ( K e. ( 2 ..^ N ) <-> ( K e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ K < N ) )
2 eluz2nn 
 |-  ( K e. ( ZZ>= ` 2 ) -> K e. NN )
3 2 3ad2ant1 
 |-  ( ( K e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ K < N ) -> K e. NN )
4 1 3 sylbi 
 |-  ( K e. ( 2 ..^ N ) -> K e. NN )