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

Each result cited below is universally quantified over the data in its own statement and is applied to the data indicated where it is cited.

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, by Commutative Rings, Fields and Ordered Fields: Standard Notation §numerals, an element $n$ of $\mathbb{N}_{0}$ standing in $F$ denotes its image $n_{F}$, $0_{F}$ and $1_{F}$ are the zero and the unit of $F$, and the image of a sum is the sum of the images; so $(n+1)_{F}=n_{F}+1$ for every $n\in\mathbb{N}_{0}$. As $2=1+1$ in $\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §digits, the same clause gives $2_{F}=1+1$, that is, $2=1+1$ in $F$; and $u+u=1\cdot u+1\cdot u=(1+1)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.

Naturals. Let $A$ be the set of those $n\in\mathbb{N}_{0}$ with $0\le n_{F}$. Then $0\in A$, since $0_{F}=0$ and $\le$ is reflexive. Let $n\in A$. As $0<1$ by Rules of Arithmetic and Order in an Ordered Field §squares and $0\le n_{F}$, Strict sum gives $0=0+0<1+n_{F}=n_{F}+1=(n+1)_{F}$ by the second preliminary fact; in particular $0\le(n+1)_{F}$, so $n+1\in A$. By induction from $0$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction), $A=\mathbb{N}_{0}$, and the step shows $0<(m+1)_{F}$ for every $m\in\mathbb{N}_{0}$. Now let $n\in\mathbb{N}$. If $n=1$, then $n=0+1$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §zero; otherwise $n=m+1$ for some $m\in\mathbb{N}$ by Arithmetic and Order of the Natural Numbers §predecessor. In both cases $0<n_{F}$. Thus, in $F$, $0\le n$ for every $n\in\mathbb{N}_{0}$, and $0<n$ for every $n\in\mathbb{N}$.

Halving. By Rules of Arithmetic and Order in an Ordered Field §midpoint, $0<1+1$, and $1+1=2$ in $F$ by the second preliminary fact; so $0<2$ in $F$, hence $2\neq0$ in $F$, 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})$.