Proof of Elementary Arithmetic in an Ordered Field

Field axioms are numbered as in Field and the two order axioms as in Ordered Field. The order is a total order, hence reflexive, transitive, antisymmetric and total.

We first record two field identities. For every $c\in F$ we have $c\cdot 0=0$: by axioms 2 and 9, $c\cdot 0=c(0+0)=c\cdot 0+c\cdot 0$, and adding the additive inverse of $c\cdot 0$ from axiom 3 gives $0=c\cdot 0$. And $c(-d)=-(cd)$ for all $c,d\in F$: by axioms 9 and 3 and the identity just proved, $cd+c(-d)=c(d+(-d))=c\cdot 0=0$, so $c(-d)$ is an additive inverse of $cd$.

Claim 1. By axiom 6, $1\ne 0$. Let $t=|1|$ be the absolute value of $1$. Claim 1 of Properties of the Absolute Value in an Ordered Field gives $0\le t$, and $t\ne 0$ because that claim yields $t=0$ only for $1=0$. Claim 4 of the same lemma with $x=y=1$, together with $1\cdot 1=1$ from axiom 6, gives $t=|1\cdot 1|=|1|\,|1|=t\,t$. Multiplying by the inverse $t^{-1}$ of axiom 7 and using axioms 5 and 6,

Hence $|1|=1$ and $0\le 1$.

Claim 2. From $0\le b$ and order axiom 1 with $c=a$ we get $0+a\le b+a$. By axioms 2 and 4, $0+a=a$ and $b+a=a+b$, so $a\le a+b$; transitivity with $0\le a$ gives $0\le a+b$.

Claim 3. Suppose $x\le y$. Order axiom 1 with $c=-x$ gives $x+(-x)\le y+(-x)$, that is, $0\le y-x$ by axiom 3. Conversely suppose $0\le y-x$. Order axiom 1 with $c=x$ gives $0+x\le (y+(-x))+x$; the left-hand side is $x$ by axioms 2 and 4, and the right-hand side is $y+((-x)+x)=y+0=y$ by axioms 1, 2, 3 and 4. Hence $x\le y$.

Claim 4. By axiom 7 there is $a^{-1}$ with $a\,a^{-1}=1$, and $a^{-1}\ne 0$, since $a^{-1}=0$ would give $1=a\cdot 0=0$ by the recorded identity, contradicting axiom 6.

Suppose $0\le a^{-1}$ fails. As the order is total, $a^{-1}\le 0$, so claim 3 applied with $x=a^{-1}$ and $y=0$ gives $0\le 0-a^{-1}$, and $0-a^{-1}=-a^{-1}$ by axioms 2 and 4. Order axiom 2 applied to $0\le a$ and $0\le -a^{-1}$ gives

using the recorded identity. By claim 3 with $x=1$ and $y=0$, this says $1\le 0$; with claim 1 and antisymmetry we get $1=0$, contradicting axiom 6. Hence $0\le a^{-1}$.

Claim 5. By claim 3, $0\le y-x$. Order axiom 2 applied to $0\le a$ and $0\le y-x$ gives $0\le a(y-x)$, and by axiom 9 and the recorded identity $a(y-x)=ay+a(-x)=ay+(-(ax))=ay-ax$. Claim 3 applied with $x$ replaced by $ax$ and $y$ by $ay$ now gives $ax\le ay$.