Reason: Initial publication: all claims derived from the ordered-field axioms, via the equivalence of a<=b with a^2<=b^2 for nonnegative elements.
Proof
Throughout, F is an ordered field: a field together with a total order≤ such that a≤b implies a+c≤b+c, and 0≤a together with 0≤b implies 0≤ab. Absolute values are those of that definition. We first record some consequences of these axioms.
(a)u≤0 if and only if 0≤−u. Indeed, adding −u to u≤0 gives 0≤−u, and adding u to 0≤−u gives u≤0.
(b) If u≤v then −v≤−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≤c and u≤v then cu≤cv: from u≤v we get 0≤v−u, hence 0≤c(v−u)=cv−cu, and adding cu gives cu≤cv.
(e)0≤u2 for every u: if 0≤u this is the second order axiom, and otherwise u≤0 by totality, so 0≤−u by (a) and 0≤(−u)(−u)=u2 by (c).
(f) If 0≤a and 0≤b, then a≤b if and only if a2≤b2. For the forward direction, (d) with c=a gives a2≤ab and (d) with c=b gives ab≤b2, so a2≤b2 by transitivity. Conversely, suppose a2≤b2 and, for a contradiction, that a≤b fails. By totality b≤a, and a=b. The forward direction applied to b≤a gives b2≤a2, so a2=b2 by antisymmetry, that is (a−b)(a+b)=a2−b2=0. Since a=b we have a−b=0, so multiplying by its inverse gives a+b=0, that is a=−b. Then 0≤b gives a≤0 by (a), so a=0 by antisymmetry, whence b=−a=0 and a=b, a contradiction. In particular, if 0≤a, 0≤b and a2=b2, then a=b.
(g)∣u∣2=u2 for every u, because ∣u∣ is u or −u and (−u)(−u)=u2 by (c).
Claim 1. That ∣x∣ is x or −x is immediate from the definition. If 0≤x then ∣x∣=x, so 0≤∣x∣; otherwise x≤0 by totality, so 0≤−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≤0, so ∣0∣=0.
Claim 2. If 0≤x fails, then x≤0 by totality, so 0≤−x by (a); hence ∣−x∣=−x and ∣x∣=−x, and the two agree. If 0≤x and x=0, then ∣−x∣=∣0∣=0=∣x∣. If 0≤x and x=0, then −x≤0 by (a); moreover 0≤−x would force −x=0 by antisymmetry and hence x=0, so 0≤−x fails and ∣−x∣=−(−x)=x=∣x∣.
Claim 3. If 0≤x then ∣x∣=x, so x≤∣x∣ by reflexivity, and −∣x∣=−x≤0≤x by (a) and transitivity. If 0≤x fails then x≤0 by totality and ∣x∣=−x, so x≤0≤−x=∣x∣ by (a) and transitivity, while −∣x∣=−(−x)=x≤x.
Claim 4. By claim 1 we have 0≤∣xy∣, and 0≤∣x∣, 0≤∣y∣, so 0≤∣x∣∣y∣ by the second order axiom. By (g),
∣xy∣2=(xy)2=x2y2=∣x∣2∣y∣2=(∣x∣∣y∣)2.
Since both ∣xy∣ and ∣x∣∣y∣ are nonnegative, (f) gives ∣xy∣=∣x∣∣y∣.
Claim 5. From 0≤∣y∣ and (d) or directly by adding ∣x∣ we get ∣x∣≤∣x∣+∣y∣, and 0≤∣x∣, so 0≤∣x∣+∣y∣ by transitivity; also 0≤∣x+y∣ by claim 1. By (f) it suffices to prove ∣x+y∣2≤(∣x∣+∣y∣)2. Using (g), claim 4 and the field axioms,
By claim 3 applied to the element xy we have xy≤∣xy∣; adding xy and then ∣xy∣ gives xy+xy≤∣xy∣+∣xy∣. Adding x2+y2 to both sides gives the required inequality.
Claim 6. Suppose ∣x∣≤c. By claim 3, x≤∣x∣, so x≤c by transitivity; and −c≤−∣x∣ by (b), while −∣x∣≤x by claim 3, so −c≤x by transitivity. Conversely suppose −c≤x and x≤c. If 0≤x then ∣x∣=x≤c. Otherwise ∣x∣=−x, and applying (b) to −c≤x gives −x≤c, that is ∣x∣≤c.
Claim 7. By claim 5 applied to x−y and y,
∣x∣=∣(x−y)+y∣≤∣x−y∣+∣y∣,
and adding −∣y∣ gives ∣x∣−∣y∣≤∣x−y∣. Interchanging x and y gives ∣y∣−∣x∣≤∣y−x∣, and ∣y−x∣=∣−(x−y)∣=∣x−y∣ by claim 2. Applying (b) to ∣y∣−∣x∣≤∣x−y∣ and using −(∣y∣−∣x∣)=∣x∣−∣y∣ yields −∣x−y∣≤∣x∣−∣y∣. Thus −∣x−y∣≤∣x∣−∣y∣≤∣x−y∣, and claim 6 applied with c=∣x−y∣ gives ∣x∣−∣y∣≤∣x−y∣.