Metamath Proof Explorer


Theorem nnabscl

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 )

Proof

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 )