Description: The absolute value of a nonzero integer is a positive integer. (Contributed by Paul Chapman, 21-Mar-2011) (Proof shortened by Andrew Salmon, 25-May-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nnabscl | |- ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zabscl | |- ( N e. ZZ -> ( abs ` N ) e. ZZ ) |
|
| 2 | 1 | adantr | |- ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. ZZ ) |
| 3 | zcn | |- ( N e. ZZ -> N e. CC ) |
|
| 4 | absgt0 | |- ( N e. CC -> ( N =/= 0 <-> 0 < ( abs ` N ) ) ) |
|
| 5 | 3 4 | syl | |- ( N e. ZZ -> ( N =/= 0 <-> 0 < ( abs ` N ) ) ) |
| 6 | 5 | biimpa | |- ( ( N e. ZZ /\ N =/= 0 ) -> 0 < ( abs ` N ) ) |
| 7 | elnnz | |- ( ( abs ` N ) e. NN <-> ( ( abs ` N ) e. ZZ /\ 0 < ( abs ` N ) ) ) |
|
| 8 | 2 6 7 | sylanbrc | |- ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN ) |