Ring of rational integers is Euclidean with norm equal to absolute value

Statement

Consider $\mathbb {Z}$ , the ring of rational integers. This is a Euclidean domain, with Euclidean norm given by:

$x\mapsto |x|$ .

In other words, for any integers $a,b\in \mathbb {Z}$ with $b\neq 0$ , there exist $q,r\in \mathbb {Z}$ with:

$a=bq+r$

and either $r=0$ or $|r|<|b|$ .

Other simple observations about the absolute value norm include:

The absolute value norm is an automorphism-invariant norm: This holds trivially, since the ring of rational integers has no non-identity automorphism.
The absolute value norm is a positive norm: It is nonzero on all nonzero elements of the ring.
The absolute value norm is a multiplicative norm: The absolute value of a product of nonzero integers is the product of their absolute values.
The absolute value norm is a multiplicatively monotone norm: The absolute value of a product of nonzero integers is at least equal to the maximum of their absolute values. This follows from the previous two facts, and the observation that multiplicative and positive implies multiplicatively monotone.
The absolute value norm takes the same value on associate elements. Further information: multiplicatively monotone norm is constant on associate classes
The absolute value norm is not uniquely Euclidean. If $a$ divides $b$ evenly, then the Euclidean division is unique. Otherwise, there are two solution pairs $(q,r)$ . Further information: Multiplicatively monotone Euclidean norm admits unique Euclidean division for exact divisor.