Proof of Properties of the Absolute Value in an Ordered Field

Attribution. The preliminary facts (a)--(g) and the proofs of claims 1--8 below are reproduced from the published proof of the preceding version of this lemma, published under the label lem:absolute-value-properties-2026a; only claim 9 and this note were new there. The present text is copied from the proof version of lem:absolute-value-properties-2026c, with claim 8 changed to refer to the real numbers of def:real-numbers-c54-2026c.

Throughout, $F$ is an ordered field: a field together with a total order $\le$ such that $a\le b$ implies $a+c\le b+c$, and $0\le a$ together with $0\le b$ implies $0\le ab$. Absolute values are those of that definition. As in the statement, $s<t$ abbreviates $s\le t$ together with $s\ne t$. We first record some consequences of these axioms.

(a) $u\le 0$ if and only if $0\le -u$. Indeed, adding $-u$ to $u\le0$ gives $0\le-u$, and adding $u$ to $0\le-u$ gives $u\le0$.

(b) If $u\le v$ then $-v\le-u$: add $-u-v$ to both sides.

(c) $(-u)v=-(uv)$ and $(-u)(-v)=uv$, since $uv+(-u)v=(u+(-u))v=0$ and the same identity applied twice.

(d) If $0\le c$ and $u\le v$ then $cu\le cv$: from $u\le v$ we get $0\le v-u$, hence $0\le c(v-u)=cv-cu$, and adding $cu$ gives $cu\le cv$.

(e) $0\le u^{2}$ for every $u$: if $0\le u$ this is the second order axiom, and otherwise $u\le0$ by totality, so $0\le-u$ by (a) and $0\le(-u)(-u)=u^{2}$ by (c).

(f) If $0\le a$ and $0\le b$, then $a\le b$ if and only if $a^{2}\le b^{2}$. For the forward direction, (d) with $c=a$ gives $a^{2}\le ab$ and (d) with $c=b$ gives $ab\le b^{2}$, so $a^{2}\le b^{2}$ by transitivity. Conversely, suppose $a^{2}\le b^{2}$ and, for a contradiction, that $a\le b$ fails. By totality $b\le a$, and $a\ne b$. The forward direction applied to $b\le a$ gives $b^{2}\le a^{2}$, so $a^{2}=b^{2}$ by antisymmetry, that is $(a-b)(a+b)=a^{2}-b^{2}=0$. Since $a\ne b$ we have $a-b\ne0$, so multiplying by its inverse gives $a+b=0$, that is $a=-b$. Then $0\le b$ gives $a\le0$ by (a), so $a=0$ by antisymmetry, whence $b=-a=0$ and $a=b$, a contradiction. In particular, if $0\le a$, $0\le b$ and $a^{2}=b^{2}$, then $a=b$.

(g) $|u|^{2}=u^{2}$ for every $u$, because $|u|$ is $u$ or $-u$ and $(-u)(-u)=u^{2}$ by (c).

Claim 1. That $|x|$ is $x$ or $-x$ is immediate from the definition. If $0\le x$ then $|x|=x$, so $0\le|x|$; otherwise $x\le0$ by totality, so $0\le-x=|x|$ by (a). If $|x|=0$ then either $|x|=x$, giving $x=0$, or $|x|=-x$, giving $-x=0$ and hence $x=0$. Conversely $0\le0$, so $|0|=0$.

Claim 2. If $0\le x$ fails, then $x\le0$ by totality, so $0\le-x$ by (a); hence $|{-x}|=-x$ and $|x|=-x$, and the two agree. If $0\le x$ and $x=0$, then $|{-x}|=|0|=0=|x|$. If $0\le x$ and $x\ne0$, then $-x\le0$ by (a); moreover $0\le-x$ would force $-x=0$ by antisymmetry and hence $x=0$, so $0\le-x$ fails and $|{-x}|=-(-x)=x=|x|$.

Claim 3. If $0\le x$ then $|x|=x$, so $x\le|x|$ by reflexivity, and $-|x|=-x\le0\le x$ by (a) and transitivity. If $0\le x$ fails then $x\le0$ by totality and $|x|=-x$, so $x\le0\le-x=|x|$ by (a) and transitivity, while $-|x|=-(-x)=x\le x$.

Claim 4. By claim 1 we have $0\le|xy|$, and $0\le|x|$, $0\le|y|$, so $0\le|x|\,|y|$ by the second order axiom. By (g),

$$|xy|^{2}=(xy)^{2}=x^{2}y^{2}=|x|^{2}|y|^{2}=\bigl(|x|\,|y|\bigr)^{2}.$$

Since both $|xy|$ and $|x|\,|y|$ are nonnegative, (f) gives $|xy|=|x|\,|y|$.

Claim 5. From $0\le|y|$ and (d) or directly by adding $|x|$ we get $|x|\le|x|+|y|$, and $0\le|x|$, so $0\le|x|+|y|$ by transitivity; also $0\le|x+y|$ by claim 1. By (f) it suffices to prove $|x+y|^{2}\le\bigl(|x|+|y|\bigr)^{2}$. Using (g), claim 4 and the field axioms,

$$|x+y|^{2}=(x+y)^{2}=x^{2}+(xy+xy)+y^{2},\qquad \bigl(|x|+|y|\bigr)^{2}=x^{2}+\bigl(|xy|+|xy|\bigr)+y^{2}.$$

By claim 3 applied to the element $xy$ we have $xy\le|xy|$; adding $xy$ and then $|xy|$ gives $xy+xy\le|xy|+|xy|$. Adding $x^{2}+y^{2}$ to both sides gives the required inequality.

Claim 6. Suppose $|x|\le c$. By claim 3, $x\le|x|$, so $x\le c$ by transitivity; and $-c\le-|x|$ by (b), while $-|x|\le x$ by claim 3, so $-c\le x$ by transitivity. Conversely suppose $-c\le x$ and $x\le c$. If $0\le x$ then $|x|=x\le c$. Otherwise $|x|=-x$, and applying (b) to $-c\le x$ gives $-x\le c$, that is $|x|\le c$.

Claim 7. By claim 5 applied to $x-y$ and $y$,

$$|x|=|(x-y)+y|\le|x-y|+|y| ,$$

and adding $-|y|$ gives $|x|-|y|\le|x-y|$. Interchanging $x$ and $y$ gives $|y|-|x|\le|y-x|$, and $|y-x|=|-(x-y)|=|x-y|$ by claim 2. Applying (b) to $|y|-|x|\le|x-y|$ and using $-\bigl(|y|-|x|\bigr)=|x|-|y|$ yields $-|x-y|\le|x|-|y|$. Thus $-|x-y|\le|x|-|y|\le|x-y|$, and claim 6 applied with $c=|x-y|$ gives $\bigl||x|-|y|\bigr|\le|x-y|$.

Claim 8. Claim 8 of Properties of Complex Conjugation and Modulus states that for a real number $a$, viewed as a complex number, its modulus equals $a$ if $0\le a$ and $-a$ otherwise. The real numbers there are those of The Real Numbers, over which The Complex Numbers is built, with their order; this is the ordered field $F$ of claim 8. So the value above is precisely the value assigned to $a$ by Absolute Value in an Ordered Field in $F$.

Claim 9. Suppose first that $|x|<c$, so $|x|\le c$ and $|x|\ne c$. By claim 6, $-c\le x$ and $x\le c$. If $x=c$, then $c=x\le|x|$ by claim 3, and $|x|\le c$, so $|x|=c$ by antisymmetry, contradicting $|x|\ne c$; hence $x\ne c$ and $x<c$. If $x=-c$, then $-|x|\le x=-c$ by claim 3, so $c\le|x|$ by (b) together with $-(-c)=c$ and $-(-|x|)=|x|$; with $|x|\le c$ this gives $|x|=c$ by antisymmetry, again contradicting $|x|\ne c$. Hence $-c\ne x$ and $-c<x$.

Conversely suppose $-c<x$ and $x<c$. Then $-c\le x$ and $x\le c$, so $|x|\le c$ by claim 6. Suppose $|x|=c$. By claim 1, $|x|$ equals $x$ or $-x$. In the first case $x=c$, contradicting $x\ne c$; in the second $-x=c$, hence $x=-c$, contradicting $-c\ne x$. So $|x|\ne c$, and therefore $|x|<c$.