Proof of Rules of Order in an Ordered Ring: Differences, Sums, Negatives, Products and Squares

Each result cited is universally quantified over the data in its own statement.

Preliminaries. By Ordered Rings §ordered-ring, $R$ is a commutative ring, $\le$ is a total order on $R$, and for all $a,b,c\in R$: (A) if $a\le b$ then $a+c\le b+c$; (M) if $0\le a$ and $0\le b$ then $0\le a\cdot b$. By Partial and Total Orders on a Set and the Associated Strict Relation §partial, $\le$ is transitive. By Negatives, Differences, Reciprocals and Quotients §negative, $a+(-a)=0$ and $b-a=b+(-a)$. For $a,c\in R$, associativity, commutativity and the zero law of Commutative Rings §ring give

$$(a+c)+(-c)=a+(c+(-c))=a+0=a,\quad (a+(-c))+c=a+((-c)+c)=a+(c+(-c))=a,\quad 0+a=a+0=a,$$

which we call (D). Also $-0=0$: as $0+0=0$ by the zero law of Commutative Rings §ring, $0$ is the unique $u$ with $0+u=0$ of Negatives, Differences, Reciprocals and Quotients §negative. Finally (C): if $a+c=b+c$ then $a=(a+c)+(-c)=(b+c)+(-c)=b$ by (D); so $a\neq b$ if and only if $a+c\neq b+c$.

Clause difference. If $x\le y$, then by (A) with $c=-x$, $0=x+(-x)\le y+(-x)=y-x$. If $0\le y-x$, then by (A) with $c=x$ and by (D), $x=0+x\le(y+(-x))+x=y$. Moreover $x\neq y$ if and only if $y-x\neq 0$: if $y=x$ then $y-x=x+(-x)=0$, and if $y-x=0$ then $y=(y+(-x))+x=0+x=x$ by (D). By Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-characterization, $x<y$ if and only if $x\le y$ and $x\neq y$, and $0<y-x$ if and only if $0\le y-x$ and $0\neq y-x$; so $x<y$ if and only if $0<y-x$.

Clause sum. If $x\le y$ then $x+z\le y+z$ by (A). If $x+z\le y+z$, then by (A) with $c=-z$ and by (D), $x=(x+z)+(-z)\le(y+z)+(-z)=y$. By (C), $x\neq y$ if and only if $x+z\neq y+z$; together with Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-characterization, $x<y$ if and only if $x+z<y+z$. Now let $x\le y$ and $z\le w$. Then $x+z\le y+z$ by (A), and $y+z=z+y\le w+y=y+w$ by (A) and commutativity (Commutative Rings §ring); so $x+z\le y+w$ by transitivity. If moreover $x<y$, then $x+z<y+z$ by the strict part just proved, and $y+z\le y+w$ means $y+z<y+w$ or $y+z=y+w$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §weak-strict; in the first case $x+z<y+w$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-transitive, in the second directly.

Clause negative. By Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs ($-(-y)=y$) and commutativity (Commutative Rings §ring), $(-x)-(-y)=(-x)+y=y+(-x)=y-x$. By clause difference above applied to $(x,y)$ and to $(-y,-x)$, both $x\le y$ and $-y\le-x$ are equivalent to $0\le y-x$, and both $x<y$ and $-y<-x$ are equivalent to $0<y-x$.

Clause scaling. Let $x\le y$, so $0\le y-x$ by clause difference above. If $0\le z$, then by (M) and Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs ($(a-b)\cdot c=a\cdot c-b\cdot c$), $0\le(y-x)\cdot z=y\cdot z-x\cdot z$, so $x\cdot z\le y\cdot z$ by clause difference. If $z\le0$, then $-0\le-z$ by clause negative above, that is $0\le-z$ as $-0=0$; by (M), $0\le(y-x)\cdot(-z)$. By commutativity (Commutative Rings §ring) and Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs ($(-a)\cdot b=-(a\cdot b)$, $(a-b)\cdot c=a\cdot c-b\cdot c$ and $-(a-b)=b-a$),

$$(y-x)\cdot(-z)=(-z)\cdot(y-x)=-(z\cdot(y-x))=-((y-x)\cdot z)=-(y\cdot z-x\cdot z)=x\cdot z-y\cdot z,$$

so $0\le x\cdot z-y\cdot z$ and $y\cdot z\le x\cdot z$ by clause difference.

Clause signs. By Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §zero, $0\cdot y=0$. If $x\le0\le y$, clause scaling above applied to $x\le0$ and $0\le y$ gives $x\cdot y\le0\cdot y=0$. If $x\le0$ and $y\le0$, clause scaling applied to $x\le0$ and $y\le0$ gives $0=0\cdot y\le x\cdot y$.

Clause squares. As $\le$ is total (Partial and Total Orders on a Set and the Associated Strict Relation §total), $0\le x$ or $x\le0$. If $0\le x$, then $0\le x\cdot x$ by (M); if $x\le0$, then $0\le x\cdot x$ by clause signs above with $y=x$. With $x=1$, $0\le1\cdot1=1$ by the unit law of Commutative Rings §ring. If $0\neq1$, then $0<1$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-characterization.

Clause product. Let $0\le x\le y$ and $0\le z\le w$. By clause scaling above with $x\le y$ and $0\le z$, $x\cdot z\le y\cdot z$. As $0\le x$ and $x\le y$, $0\le y$ by transitivity; so by clause scaling with $z\le w$ and $0\le y$, $z\cdot y\le w\cdot y$, that is $y\cdot z\le y\cdot w$ by commutativity (Commutative Rings §ring). By transitivity, $x\cdot z\le y\cdot w$.