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 ) |