Proof of Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima

Each result cited is universally quantified over the data in its own statement. No map or class is formed from a formula in this proof: the maps used are given by the cited results, and no choice is used.

Preliminaries. By the framing of Ordered Fields §ordered-field, $F$, with $+$, $\cdot$, $0$ and $1$, is a field and $\le$ is a total order on $F$; by Fields §field it is a commutative ring, so by the framing of Commutative Rings §ring, $F$ is a set and $+$ and $\cdot$ are binary operations on $F$. Hence $u+v\in F$ and $u\cdot v\in F$ for all $u,v\in F$, by Binary Operations on a Set §notation. Further, if $g:A\to B$ is a map and $u\in A$, then $g(u)\in B$: indeed $u\in A=\operatorname{dom}g$ by Functions, Values of a Function, and Functions from One Class to Another §map, so $(u,g(u))\in g$ by Functions, Values of a Function, and Functions from One Class to Another §value, whence $g(u)\in\operatorname{ran}g$ by Relations, Domain, Range, Inverse and Composition §range and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, and $\operatorname{ran}g\subseteq B$ by Functions, Values of a Function, and Functions from One Class to Another §map. Call this the value rule.

Clause negative. By Negatives, Differences, Reciprocals and Quotients §negative, $-x$ is the unique $w\in F$ with $x+w=0$, which exists and is unique by Additive and Multiplicative Inverses Are Unique §negative; so $-x\in F$. Likewise $-y\in F$, and then $x-y=x+(-y)\in F$ by the preliminaries.

Clause quotient. Let $y\neq0$. By Negatives, Differences, Reciprocals and Quotients §reciprocal, $y^{-1}$ is the unique $z\in F$ with $y\cdot z=1$, which exists and is unique by Additive and Multiplicative Inverses Are Unique §reciprocal; so $y^{-1}\in F$, and $x/y=x\cdot y^{-1}\in F$ by the preliminaries.

Clause absolute-value. By Absolute Value in an Ordered Field §absolute-value, $|x|=x$ if $0\le x$ and $|x|=-x$ otherwise. In the first case $|x|\in F$ as $x\in F$; in the second, $|x|\in F$ by the clause negative.

Clause powers. By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §ring-powers, applied to the commutative ring $F$ and to $x$, there is a map $p:\mathbb{N}_{0}\to F$ with $p(n)=x^{n}$ for every $n\in\mathbb{N}_{0}$, the powers being those of Powers with Exponents in the Natural Numbers with Zero §power and Powers with Exponents in the Natural Numbers with Zero §zero for the multiplication $\cdot$. For $n\in\mathbb{N}_{0}$, $x^{n}=p(n)\in F$ by the value rule.

Clause naturals. By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §images, applied to the commutative ring $F$, there is a map $\nu:\mathbb{N}_{0}\to F$ with $\nu(n)=n_{F}$ for every $n\in\mathbb{N}_{0}$, where $n_{F}$ is the image of $n$. For $n\in\mathbb{N}_{0}$, $n_{F}=\nu(n)\in F$ by the value rule.

Clause two. By Arithmetic and Order of the Natural Numbers §digits, $2=1+1$ in $\mathbb{N}_{0}$, the addition of $\mathbb{N}$ there being that of $\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §operations. Hence $2_{F}=(1+1)_{F}=1_{F}+1_{F}$ by The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products §sum, and $1_{F}$ is the unit $1$ of $F$ by The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products §constants; so $2=1+1$ in $F$. By the clause naturals, $2\in F$. By Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares §halving, $0<2$ in $F$, so $0\neq2$ by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-characterization; that is, $2\neq0$.

Clause halves. By the clause two, $2\in F$ and $2\neq0$. By the clause quotient with $y=2$, $h=2^{-1}\in F$ and $x/2=x\cdot h\in F$, and $2\cdot h=1$ by Negatives, Differences, Reciprocals and Quotients §reciprocal. Using the identities of Commutative Rings §ring (the unit law $u\cdot1=u$, distributivity, associativity and commutativity of $\cdot$, in this order, and then $2\cdot h=1$ and the unit law),

$$x/2+x/2=(x\cdot h)\cdot1+(x\cdot h)\cdot1=(x\cdot h)\cdot(1+1)=(x\cdot h)\cdot2=x\cdot(h\cdot2)=x\cdot(2\cdot h)=x\cdot1=x,$$

where $(x\cdot h)\cdot(1+1)=(x\cdot h)\cdot2$ holds as $2=1+1$ in $F$ by the clause two.

Clause minimum. Let $a,b\in F$ with $0<a$ and $0<b$. As $\le$ is a total order on the set $F$, The Maximum and Minimum of Two Elements of a Total Order §exists shows that the subset $\{a,b\}$ of $F$ has a least element, and $\min\{a,b\}$ denotes it, as in Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §least. By Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §least, $\min\{a,b\}\in\{a,b\}$, so $\min\{a,b\}=a$ or $\min\{a,b\}=b$ by The Empty Set, the Unordered Pair and the Singleton §pair. In either case $\min\{a,b\}\in F$ and $0<\min\{a,b\}$, since $a,b\in F$, $0<a$ and $0<b$. By The Maximum and Minimum of Two Elements of a Total Order §bounds, $\min\{a,b\}\le a$ and $\min\{a,b\}\le b$. Taking $c=\min\{a,b\}$ gives the last assertion.