Basic properties of the absolute value

Case $x>0$: by [L1] $\mathrm{\mid }x\mathrm{\mid }=x>0$, so $\mathrm{\mid }x\mathrm{\mid }\ge 0$ and $\mathrm{\mid }x\mathrm{\mid }\mathrm{\ne }0$; since $-x<0$ we get $\mathrm{\mid }-x\mathrm{\mid }=-(-x)=x=\mathrm{\mid }x\mathrm{\mid }$ by [L1], and $-\mathrm{\mid }x\mathrm{\mid }=-x<0<x=\mathrm{\mid }x\mathrm{\mid }$, so $-\mathrm{\mid }x\mathrm{\mid }\le x\le \mathrm{\mid }x\mathrm{\mid }$.

Case $x=0$: then $\mathrm{\mid }x\mathrm{\mid }=\mathrm{\mid }0\mathrm{\mid }=0$, so $\mathrm{\mid }x\mathrm{\mid }\ge 0$ holds with $\mathrm{\mid }x\mathrm{\mid }=0$ and $x=0$, while $\mathrm{\mid }-x\mathrm{\mid }=\mathrm{\mid }0\mathrm{\mid }=\mathrm{\mid }x\mathrm{\mid }$ and $-\mathrm{\mid }x\mathrm{\mid }=0\le 0\le 0=\mathrm{\mid }x\mathrm{\mid }$.

Case $x<0$: by [L1] $\mathrm{\mid }x\mathrm{\mid }=-x$, and [L2] gives $-x>0$, so $\mathrm{\mid }x\mathrm{\mid }>0$ and $\mathrm{\mid }x\mathrm{\mid }\mathrm{\ne }0$; here $\mathrm{\mid }-x\mathrm{\mid }=-x=\mathrm{\mid }x\mathrm{\mid }$ by [L1], and $-\mathrm{\mid }x\mathrm{\mid }=-(-x)=x\le x$ while $x<0<-x=\mathrm{\mid }x\mathrm{\mid }$, so $-\mathrm{\mid }x\mathrm{\mid }\le x\le \mathrm{\mid }x\mathrm{\mid }$.

Case $x=0$ or $y=0$: then $xy=0$, so $\mathrm{\mid }xy\mathrm{\mid }=0$, and one of $\mathrm{\mid }x\mathrm{\mid },\mathrm{\mid }y\mathrm{\mid }$ is $0$, whence $\mathrm{\mid }x\mathrm{\mid }\mathrm{\mid }y\mathrm{\mid }=0=\mathrm{\mid }xy\mathrm{\mid }$.

Case $x,y$ have the same sign (both positive or both negative): by [L4] $xy>0$, so $\mathrm{\mid }xy\mathrm{\mid }=xy$, while $\mathrm{\mid }x\mathrm{\mid }\mathrm{\mid }y\mathrm{\mid }=xy$ by [L3] (for $x,y<0$ this is $(-x)(-y)=xy$), hence $\mathrm{\mid }xy\mathrm{\mid }=\mathrm{\mid }x\mathrm{\mid }\mathrm{\mid }y\mathrm{\mid }$.

Case $x,y$ have opposite signs (one positive, one negative): by [L4] $xy<0$, so $\mathrm{\mid }xy\mathrm{\mid }=-(xy)$, while $\mathrm{\mid }x\mathrm{\mid }\mathrm{\mid }y\mathrm{\mid }=-(xy)$ by [L3] (namely $x(-y)$ or $(-x)y$), hence $\mathrm{\mid }xy\mathrm{\mid }=\mathrm{\mid }x\mathrm{\mid }\mathrm{\mid }y\mathrm{\mid }$.

By trichotomy [L2] each $x$ lies in exactly one of the cases 1.1-1.3, and in each we verified $\mathrm{\mid }x\mathrm{\mid }\ge 0$, that $\mathrm{\mid }x\mathrm{\mid }=0⟺x=0$, that $\mathrm{\mid }-x\mathrm{\mid }=\mathrm{\mid }x\mathrm{\mid }$, and that $-\mathrm{\mid }x\mathrm{\mid }\le x\le \mathrm{\mid }x\mathrm{\mid }$; hence all four hold for every $x$.

By trichotomy [L2] each pair $x,y$ lies in exactly one of the cases 1.4-1.6, and in each $\mathrm{\mid }xy\mathrm{\mid }=\mathrm{\mid }x\mathrm{\mid }\mathrm{\mid }y\mathrm{\mid }$; hence $\mathrm{\mid }xy\mathrm{\mid }=\mathrm{\mid }x\mathrm{\mid }\mathrm{\mid }y\mathrm{\mid }$ for all $x,y$.

Let $c>0$: if $\mathrm{\mid }x\mathrm{\mid }<c$ then $-c<-\mathrm{\mid }x\mathrm{\mid }\le x\le \mathrm{\mid }x\mathrm{\mid }<c$ by [step 2.1] and [L2], so $-c<x<c$; conversely if $-c<x<c$ then both $x<c$ and $-x<c$, and since $\mathrm{\mid }x\mathrm{\mid }$ equals $x$ or $-x$ by [L1], we get $\mathrm{\mid }x\mathrm{\mid }<c$, so $\mathrm{\mid }x\mathrm{\mid }<c⟺-c<x<c$.