Description: A half-open integer range starting at a nonnegative integer is a subset of the nonnegative integers. (Contributed by Alexander van der Vekens, 13-May-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fzossnn0 | |- ( M e. NN0 -> ( M ..^ N ) C_ NN0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fzossfz | |- ( M ..^ N ) C_ ( M ... N ) |
|
| 2 | fzss1 | |- ( M e. ( ZZ>= ` 0 ) -> ( M ... N ) C_ ( 0 ... N ) ) |
|
| 3 | nn0uz | |- NN0 = ( ZZ>= ` 0 ) |
|
| 4 | 2 3 | eleq2s | |- ( M e. NN0 -> ( M ... N ) C_ ( 0 ... N ) ) |
| 5 | 1 4 | sstrid | |- ( M e. NN0 -> ( M ..^ N ) C_ ( 0 ... N ) ) |
| 6 | fz0ssnn0 | |- ( 0 ... N ) C_ NN0 |
|
| 7 | 5 6 | sstrdi | |- ( M e. NN0 -> ( M ..^ N ) C_ NN0 ) |