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