Description: The absolute value of an integer is a nonnegative integer. (Contributed by NM, 27-Feb-2005) (Proof shortened by Mario Carneiro, 29-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nn0abscl | |- ( A e. ZZ -> ( abs ` A ) e. NN0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zre | |- ( A e. ZZ -> A e. RR ) |
|
| 2 | absz | |- ( A e. RR -> ( A e. ZZ <-> ( abs ` A ) e. ZZ ) ) |
|
| 3 | 1 2 | syl | |- ( A e. ZZ -> ( A e. ZZ <-> ( abs ` A ) e. ZZ ) ) |
| 4 | 3 | ibi | |- ( A e. ZZ -> ( abs ` A ) e. ZZ ) |
| 5 | zcn | |- ( A e. ZZ -> A e. CC ) |
|
| 6 | absge0 | |- ( A e. CC -> 0 <_ ( abs ` A ) ) |
|
| 7 | 5 6 | syl | |- ( A e. ZZ -> 0 <_ ( abs ` A ) ) |
| 8 | elnn0z | |- ( ( abs ` A ) e. NN0 <-> ( ( abs ` A ) e. ZZ /\ 0 <_ ( abs ` A ) ) ) |
|
| 9 | 4 7 8 | sylanbrc | |- ( A e. ZZ -> ( abs ` A ) e. NN0 ) |