Description: If an integer is greater than or equal to 2, then it is a nonnegative integer. (Contributed by AV, 27-Aug-2018) (Proof shortened by AV, 3-Nov-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eluzge2nn0 | |- ( N e. ( ZZ>= ` 2 ) -> N e. NN0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eluz2nn | |- ( N e. ( ZZ>= ` 2 ) -> N e. NN ) |
|
| 2 | 1 | nnnn0d | |- ( N e. ( ZZ>= ` 2 ) -> N e. NN0 ) |