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	$$⊢\left(N\in \mathbb{Z}\wedge N\ne 0\right)\to \left|N\right|\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		zabscl	$$⊢N\in \mathbb{Z}\to \left|N\right|\in \mathbb{Z}$$
2	1	adantr	$$⊢\left(N\in \mathbb{Z}\wedge N\ne 0\right)\to \left|N\right|\in \mathbb{Z}$$
3		zcn	$$⊢N\in \mathbb{Z}\to N\in ℂ$$
4		absgt0	$$⊢N\in ℂ\to \left(N\ne 0\leftrightarrow 0<\left|N\right|\right)$$
5	3 4	syl	$$⊢N\in \mathbb{Z}\to \left(N\ne 0\leftrightarrow 0<\left|N\right|\right)$$
6	5	biimpa	$$⊢\left(N\in \mathbb{Z}\wedge N\ne 0\right)\to 0<\left|N\right|$$
7		elnnz	$$⊢\left|N\right|\in \mathbb{N}\leftrightarrow \left(\left|N\right|\in \mathbb{Z}\wedge 0<\left|N\right|\right)$$
8	2 6 7	sylanbrc	$$⊢\left(N\in \mathbb{Z}\wedge N\ne 0\right)\to \left|N\right|\in \mathbb{N}$$