Description: Half-open integer ranges starting with 0 are subsets of NN0. (Contributed by Thierry Arnoux, 8-Oct-2018) (Proof shortened by JJ, 1-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fzo0ssnn0 | |- ( 0 ..^ N ) C_ NN0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elfzonn0 | |- ( k e. ( 0 ..^ N ) -> k e. NN0 ) |
|
| 2 | 1 | ssriv | |- ( 0 ..^ N ) C_ NN0 |