Metamath Proof Explorer


Theorem fzssnn

Description: Finite sets of sequential integers starting from a natural are a subset of the positive integers. (Contributed by Thierry Arnoux, 4-Aug-2017)

Ref Expression
Assertion fzssnn
|- ( M e. NN -> ( M ... N ) C_ NN )

Proof

Step Hyp Ref Expression
1 fzss1
 |-  ( M e. ( ZZ>= ` 1 ) -> ( M ... N ) C_ ( 1 ... N ) )
2 nnuz
 |-  NN = ( ZZ>= ` 1 )
3 1 2 eleq2s
 |-  ( M e. NN -> ( M ... N ) C_ ( 1 ... N ) )
4 fz1ssnn
 |-  ( 1 ... N ) C_ NN
5 3 4 sstrdi
 |-  ( M e. NN -> ( M ... N ) C_ NN )