Metamath Proof Explorer

Theorem elfz2nn

Description: A member of a finite set of sequential integers starting at 2 is a positive integer. (Contributed by AV, 5-Apr-2026)

Ref Expression
Assertion elfz2nn 
|- ( K e. ( 2 ... N ) -> K e. NN )

Proof

Step Hyp Ref Expression
1 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
2 fzss1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ... N ) C_ ( 1 ... N ) )
3 1 2 ax-mp 
 |-  ( 2 ... N ) C_ ( 1 ... N )
4 3 sseli 
 |-  ( K e. ( 2 ... N ) -> K e. ( 1 ... N ) )
5 elfznn 
 |-  ( K e. ( 1 ... N ) -> K e. NN )
6 4 5 syl 
 |-  ( K e. ( 2 ... N ) -> K e. NN )