Absolute value in $\mathbb{Z}$: $|a| \ge 0$; $|a| = 0$ exactly when $a = 0$; $|-a| = |a|$; $|ab| = |a|\,|b|$; $-|a| \le a \le |a|$; and $|a| \le c$ exactly when $-c \le a \le c$

For every $x$: $0 \le x$ if and only if $-x \le 0$, and $x \le 0$ if and only if $0 \le -x$. Adding $-x$ to $0 \le x$ gives $-x \le 0$, and adding $x$ to $-x \le 0$ gives back $0 \le x$; the second equivalence is the same computation with $x$ and $-x$ interchanged, using $-(-x) = x$.

If $0 \le u$ and $0 \le v$ then $0 \le uv$. If $u = 0$ or $v = 0$ then $uv = 0$; otherwise $0 < u$ and $0 < v$, so $0 < uv$ because positives are closed under multiplication.

By totality, at least one of $0 \le a$ and $a \le 0$ holds, and correspondingly $|a| = a$ or $|a| = -a$; this is the case split used throughout, and it is exhaustive.

Case $a \ge 0$: $|a| = a \ge 0$.

Case $a \le 0$: $|a| = -a$, and $0 \le -a$ by step 1.1, so $|a| \ge 0$.

If $a = 0$ then $|a| = 0$ by the first clause. Conversely, if $|a| = 0$ then in the case $a \ge 0$ we get $a = |a| = 0$, and in the case $a \le 0$ we get $-a = |a| = 0$, whence $a = -(-a) = -0 = 0$. This is claim 2.

Claim 3. If $a \ge 0$ then $-a \le 0$ by step 1.1, so $|-a| = -(-a) = a = |a|$. If $a \le 0$ then $0 \le -a$ by step 1.1, so $|-a| = -a = |a|$.

Claim 4, case $a \ge 0$ and $b \ge 0$: $ab \ge 0$ by step 1.2, so $|ab| = ab = |a|\,|b|$.

Claim 4, case $a \ge 0$ and $b \le 0$: $0 \le -b$ by step 1.1, so $0 \le a(-b) = -(ab)$ by step 1.2, hence $ab \le 0$ by step 1.1 again; therefore $|ab| = -(ab) = a(-b) = |a|\,|b|$.

Claim 4, case $a \le 0$ and $b \ge 0$: the same computation with the factors interchanged, using commutativity of multiplication, gives $|ab| = (-a)b = |a|\,|b|$.

Claim 4, case $a \le 0$ and $b \le 0$: $0 \le -a$ and $0 \le -b$ by step 1.1, so $0 \le (-a)(-b) = ab$ by step 1.2, hence $|ab| = ab = (-a)(-b) = |a|\,|b|$.

Claim 5. If $a \ge 0$ then $|a| = a$, so $a \le |a|$; and $-|a| = -a \le 0 \le a$ by step 1.1, so $-|a| \le a$ by transitivity. If $a \le 0$ then $|a| = -a$ and $0 \le -a$ by step 1.1, so $a \le 0 \le |a|$ by transitivity; and $-|a| = -(-a) = a \le a$.

Claim 6, from right to left: suppose $-c \le a \le c$. If $a \ge 0$ then $|a| = a \le c$. If $a \le 0$ then $|a| = -a$, and adding $c - a$ to $-c \le a$ gives $-a \le c$, that is $|a| \le c$.

Claim 1 holds: $|a| \ge 0$ in both cases.

The four sign combinations of step 2.4 to step 2.7 exhaust the possibilities by totality, so claim 4 holds for all $a, b$.

Claim 6, from left to right: suppose $|a| \le c$. Then $a \le |a| \le c$ by step 2.8 and transitivity. Adding $-c - |a|$ to $|a| \le c$ gives $-c \le -|a|$, and $-|a| \le a$ by step 2.8, so $-c \le a$ by transitivity.

Every one of the six claims is now established, claim 6 by its two halves.