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$. Additive inverses are unique: if $u+v=0$ and $u+w=0$, then $v=v+0=v+(u+w)=(v+u)+w=0+w=w$ by axioms 1, 2 and 4. Hence $c(-d)=-(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,

$$1=t\,t^{-1}=(t\,t)\,t^{-1}=t\,(t\,t^{-1})=t\cdot 1=t .$$

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

$$0\le a(-a^{-1})=-(a\,a^{-1})=-1 ,$$

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$.

Claim 6. First, $0\le s\cdot s$ for every $s\in F$. As the order is total, $0\le s$ or $s\le0$. If $0\le s$, order axiom 2 gives $0\le s\cdot s$. If $s\le0$, claim 3 with $x=s$ and $y=0$ gives $0\le0-s=-s$, so order axiom 2 gives $0\le(-s)(-s)$, and $(-s)(-s)=s\cdot s$ by claim 2 of Zero Products and Elementary Identities in a Field.

Next, apply claim 5 of Zero Products and Elementary Identities in a Field to the pairs $(x,y)$ and $(x,-y)$. Use $x(-y)=-(xy)$, recorded at the start of this proof, and $(-y)(-y)=y^{2}$, by claim 2 of that lemma. This gives

$$(x+y)^{2}=x^{2}+(xy+xy)+y^{2},\qquad(x-y)^{2}=x^{2}+\bigl(-(xy)+(-(xy))\bigr)+y^{2}.$$

Adding these and using the field axioms gives $(x+y)^{2}+(x-y)^{2}=(1+1)x^{2}+(1+1)y^{2}=2\,(x^{2}+y^{2})$. Hence $2\,(x^{2}+y^{2})-(x-y)^{2}=(x+y)^{2}$. This is nonnegative by the first step, applied with $s=x+y$, so claim 3, applied to $(x-y)^{2}$ and $2\,(x^{2}+y^{2})$, gives $(x-y)^{2}\le2\,(x^{2}+y^{2})$.