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 ) |
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 ) |