Theorem nn0abscl

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\in \mathbb{Z}\to \left|A\right|\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		zre	$$⊢A\in \mathbb{Z}\to A\in ℝ$$
2		absz	$$⊢A\in ℝ\to \left(A\in \mathbb{Z}\leftrightarrow \left|A\right|\in \mathbb{Z}\right)$$
3	1 2	syl	$$⊢A\in \mathbb{Z}\to \left(A\in \mathbb{Z}\leftrightarrow \left|A\right|\in \mathbb{Z}\right)$$
4	3	ibi	$$⊢A\in \mathbb{Z}\to \left|A\right|\in \mathbb{Z}$$
5		zcn	$$⊢A\in \mathbb{Z}\to A\in ℂ$$
6		absge0	$$⊢A\in ℂ\to 0\le \left|A\right|$$
7	5 6	syl	$$⊢A\in \mathbb{Z}\to 0\le \left|A\right|$$
8		elnn0z	$$⊢\left|A\right|\in {\mathbb{N}}_0\leftrightarrow \left(\left|A\right|\in \mathbb{Z}\wedge 0\le \left|A\right|\right)$$
9	4 7 8	sylanbrc	$$⊢A\in \mathbb{Z}\to \left|A\right|\in {\mathbb{N}}_0$$