Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 elfzelz 
 |-  ( K e. ( 1 ... N ) -> K e. ZZ )
2 elfzle1 
 |-  ( K e. ( 1 ... N ) -> 1 <_ K )
3 elnnz1 
 |-  ( K e. NN <-> ( K e. ZZ /\ 1 <_ K ) )
4 1 2 3 sylanbrc 
 |-  ( K e. ( 1 ... N ) -> K e. NN )