Absolute value in $\mathbb{Z}$: $\mathrm{\mid }a\mathrm{\mid }\ge 0$; $\mathrm{\mid }a\mathrm{\mid }=0$ exactly when $a=0$; $\mathrm{\mid }-a\mathrm{\mid }=\mathrm{\mid }a\mathrm{\mid }$; $\mathrm{\mid }ab\mathrm{\mid }=\mathrm{\mid }a\mathrm{\mid }\mathrm{\mid }b\mathrm{\mid }$; $-\mathrm{\mid }a\mathrm{\mid }\le a\le \mathrm{\mid }a\mathrm{\mid }$; and $\mathrm{\mid }a\mathrm{\mid }\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 $\mathrm{\mid }a\mathrm{\mid }=a$ or $\mathrm{\mid }a\mathrm{\mid }=-a$; this is the case split used throughout, and it is exhaustive.

Case $a\ge 0$: $\mathrm{\mid }a\mathrm{\mid }=a\ge 0$.

Case $a\le 0$: $\mathrm{\mid }a\mathrm{\mid }=-a$, and $0\le -a$ by step 1.1, so $\mathrm{\mid }a\mathrm{\mid }\ge 0$.

If $a=0$ then $\mathrm{\mid }a\mathrm{\mid }=0$ by the first clause. Conversely, if $\mathrm{\mid }a\mathrm{\mid }=0$ then in the case $a\ge 0$ we get $a=\mathrm{\mid }a\mathrm{\mid }=0$, and in the case $a\le 0$ we get $-a=\mathrm{\mid }a\mathrm{\mid }=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 $\mathrm{\mid }-a\mathrm{\mid }=-(-a)=a=\mathrm{\mid }a\mathrm{\mid }$. If $a\le 0$ then $0\le -a$ by step 1.1, so $\mathrm{\mid }-a\mathrm{\mid }=-a=\mathrm{\mid }a\mathrm{\mid }$.

Claim 4, case $a\ge 0$ and $b\ge 0$: $ab\ge 0$ by step 1.2, so $\mathrm{\mid }ab\mathrm{\mid }=ab=\mathrm{\mid }a\mathrm{\mid }\mathrm{\mid }b\mathrm{\mid }$.

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 $\mathrm{\mid }ab\mathrm{\mid }=-(ab)=a(-b)=\mathrm{\mid }a\mathrm{\mid }\mathrm{\mid }b\mathrm{\mid }$.

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

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 $\mathrm{\mid }ab\mathrm{\mid }=ab=(-a)(-b)=\mathrm{\mid }a\mathrm{\mid }\mathrm{\mid }b\mathrm{\mid }$.

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

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

Claim 1 holds: $\mathrm{\mid }a\mathrm{\mid }\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 $\mathrm{\mid }a\mathrm{\mid }\le c$. Then $a\le \mathrm{\mid }a\mathrm{\mid }\le c$ by step 2.8 and transitivity. Adding $-c-\mathrm{\mid }a\mathrm{\mid }$ to $\mathrm{\mid }a\mathrm{\mid }\le c$ gives $-c\le -\mathrm{\mid }a\mathrm{\mid }$, and $-\mathrm{\mid }a\mathrm{\mid }\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.