Proof of Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Halving, Reciprocals, Absolute Values and Squares

The order $\le$ of $F$ is a total order (Ordered Fields §ordered-field), and so in particular reflexive, antisymmetric and transitive (Partial and Total Orders on a Set and the Associated Strict Relation §partial). We use Rules of Arithmetic and Order in an Ordered Field for $F$. Two preliminary facts are needed.

First, for $u\in F$ we have $u^{2}=u\cdot u$. This holds by Powers with Exponents in the Natural Numbers with Zero §power and Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §recursion, because $2=1+1$ in $\mathbb{N}$ (Arithmetic and Order of the Natural Numbers §digits).

Second, the element $2$ of $F$ is $\kappa_{F}(2)$ by Ordinary Mathematical Language for Analysis: Sets, Maps, Numbers and Ordered Fields §fields. This equals $2_{F}$ by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §ordered, and by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §naturals we have $2_{F}=1_{F}+1_{F}=1+1$. Hence $2=1+1$ in $F$, and $u+u=2u$ for $u\in F$.

Mixed. Let $x\le y$ and $y<z$. Then $y\le z$ and $y\neq z$ (Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-characterization), so $x\le z$ by transitivity. If $x=z$, then $z\le y$ and $y\le z$, so $y=z$ by antisymmetry, a contradiction. Hence $x\neq z$, and $x<z$. The case $x<y$, $y\le z$ is symmetric: there $x\le z$, and $x=z$ would give $y\le x\le y$, so $x=y$.

Strict sum. By Rules of Arithmetic and Order in an Ordered Field §order-sum, $x<y$ gives $x+z<y+z$, and $z\le w$ gives $y+z\le y+w$. Then $x+z<y+w$ by Mixed.

Strict negative. By Rules of Arithmetic and Order in an Ordered Field §order-negative, $x\le y$ if and only if $-y\le-x$. Also $x\neq y$ if and only if $-y\neq-x$, since $-(-u)=u$ (Rules of Arithmetic and Order in an Ordered Field §signs). The claim follows by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-characterization.

Positive product. If $0<x$ and $0<y$, then $0\cdot y<x\cdot y$ by Rules of Arithmetic and Order in an Ordered Field §order-product, and $0\cdot y=0$ by Rules of Arithmetic and Order in an Ordered Field §zero. The nonnegative case is part of Ordered Rings §ordered-ring.

Nonnegative scaling. From $x\le y$ we get $0\le y-x$ by Rules of Arithmetic and Order in an Ordered Field §order-sum. Then $0\le(y-x)z$ by Ordered Rings §ordered-ring, and $(y-x)z=yz-xz$ by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs. Thus $xz\le yz$, again by Rules of Arithmetic and Order in an Ordered Field §order-sum.

Halving. By Rules of Arithmetic and Order in an Ordered Field §midpoint, $0<1+1=2$, so $2\neq0$ and $2^{-1}$ exists (Negatives, Differences, Reciprocals and Quotients §reciprocal). Let $0<x$. Then Rules of Arithmetic and Order in an Ordered Field §midpoint, applied to $0<x$, gives $0<(0+x)/2<x$, that is $0<x/2<x$. Moreover, by distributivity, $1+1=2$ (the second preliminary fact) and $2^{-1}\cdot2=1$, we have $x/2+x/2=x(2^{-1}+2^{-1})=x\,2^{-1}(1+1)=x\,2^{-1}\cdot2=x$.

Reciprocal order. Let $0<x\le y$. Then $0<y$ by Mixed, so $0<y^{-1}$ by Rules of Arithmetic and Order in an Ordered Field §positive-reciprocal. By Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §weak-strict, either $x<y$ or $x=y$. In the first case $y^{-1}<x^{-1}$ by Rules of Arithmetic and Order in an Ordered Field §positive-reciprocal; in the second $y^{-1}=x^{-1}$. In both cases $y^{-1}\le x^{-1}$.

Absolute strict. Suppose $|x|<y$. Since $-|x|\le x\le|x|$ (Rules of Arithmetic and Order in an Ordered Field §absolute-value), we get $x<y$ by Mixed. Also $-y<-|x|$ by Strict negative, so $-y<x$ by Mixed. Conversely, suppose $-y<x$ and $x<y$. By Absolute Value in an Ordered Field §absolute-value, $|x|=x$ or $|x|=-x$. In the first case $|x|<y$ directly. In the second, Strict negative applied to $-y<x$ gives $-x<-(-y)=y$.

Reverse triangle. We have $(x-y)+y=x+((-y)+y)=x$. So $|x|\le|x-y|+|y|$ by Rules of Arithmetic and Order in an Ordered Field §triangle, and adding $-|y|$ gives $|x|-|y|\le|x-y|$ (Rules of Arithmetic and Order in an Ordered Field §order-sum). Exchanging $x$ and $y$ gives $|y|-|x|\le|y-x|$. Here $y-x=-(x-y)$ by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs, so $|y-x|=|x-y|$ by Rules of Arithmetic and Order in an Ordered Field §absolute-value. Also $|y|-|x|=-(|x|-|y|)$ by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs, so Rules of Arithmetic and Order in an Ordered Field §order-negative and Rules of Arithmetic and Order in an Ordered Field §signs give $-|x-y|\le|x|-|y|$. The last part of Rules of Arithmetic and Order in an Ordered Field §absolute-value now gives $\big||x|-|y|\big|\le|x-y|$.

Triangle through a third point. We have $x-y=(x-z)+(z-y)$, since $(-z)+z=0$. Apply Rules of Arithmetic and Order in an Ordered Field §triangle.

Square of the absolute value. By Absolute Value in an Ordered Field §absolute-value, $|x|=x$ or $|x|=-x$. Thus $|x|^{2}=|x|\cdot|x|$ equals $x\cdot x$ or $(-x)(-x)=x\cdot x$ (Rules of Arithmetic and Order in an Ordered Field §signs); in both cases $|x|^{2}=x^{2}$.

Square of a difference. By Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §squares, $(x-y)^{2}=x^{2}-2_{F}\,xy+y^{2}$ and $(x+y)^{2}=x^{2}+2_{F}\,xy+y^{2}$. Adding these, the terms $\pm2_{F}\,xy$ cancel, and $(x-y)^{2}+(x+y)^{2}=(x^{2}+x^{2})+(y^{2}+y^{2})=2x^{2}+2y^{2}=2\,(x^{2}+y^{2})$. Since $(x+y)^{2}=(x+y)(x+y)\ge0$ by Rules of Arithmetic and Order in an Ordered Field §squares, Rules of Arithmetic and Order in an Ordered Field §order-sum gives $(x-y)^{2}=(x-y)^{2}+0\le(x-y)^{2}+(x+y)^{2}=2\,(x^{2}+y^{2})$.