Proof of The Absolute Value Metric on the Real Line

We verify the four conditions in the definition of a metric, using the properties of the absolute value in an ordered field, applied to the ordered field $\mathbb{R}$. Since the absolute value of an element of $\mathbb{R}$ is again an element of $\mathbb{R}$, the assignment $d_{\mathbb{R}}$ is indeed a function from $\mathbb{R}\times\mathbb{R}$ to $\mathbb{R}$. Let $s,t,r\in\mathbb{R}$.

Condition 1 (nonnegativity). Claim 1 of Properties of the Absolute Value in an Ordered Field gives $0\le|s-t|$, that is $0\le d_{\mathbb{R}}(s,t)$.

Condition 2 (vanishing exactly on the diagonal). Claim 1 of Properties of the Absolute Value in an Ordered Field gives that $|s-t|=0$ holds if and only if $s-t=0$. If $s-t=0$, then adding $t$ to both sides gives $s=t$; conversely, if $s=t$, then $s-t=t+(-t)=0$. Hence $d_{\mathbb{R}}(s,t)=0$ if and only if $s=t$.

Condition 3 (symmetry). In a field $t-s=-(s-t)$, so claim 2 of Properties of the Absolute Value in an Ordered Field gives

Condition 4 (triangle inequality). In a field $s-r=(s-t)+(t-r)$, so claim 5 of Properties of the Absolute Value in an Ordered Field gives

All four conditions hold, so $d_{\mathbb{R}}$ is a metric on $\mathbb{R}$.