Proof of The Structure of ℝ as a Field and an Ordered Ring

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

The structure. By The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum §ordered-field, $\mathbb{R}$, with $+$, $\cdot$, $0$, $1$ and $\le$, is an ordered field; these are the data of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals, whose $0$ and $1$ are the elements $0_{\mathbb{R}}$ and $1_{\mathbb{R}}$ of The Real Numbers §constants.

Clause field. Ordered fields are defined in Ordered Fields only for a set $r$ which, with $+$, $\cdot$, $0$ and $1$, is a field, together with a total order on $r$. So $\mathbb{R}$, with $+$, $\cdot$, $0$ and $1$, is a field. By Fields §field it is in particular a commutative ring, which is used below.

Clause ordered-ring. By Ordered Fields §ordered-field, $\mathbb{R}$, with $+$, $\cdot$, $0$, $1$ and $\le$, is an ordered field precisely when it is an ordered ring; since it is an ordered field, it is an ordered ring.

Clause partial-order. By The Real Numbers §reals, $\le$ is a total order on $\mathbb{R}$, hence a partial order on $\mathbb{R}$ by Partial and Total Orders on a Set and the Associated Strict Relation §total.

Clauses mul-associative, mul-commutative and add-neutral. By Arithmetic and Order Rules in the Real Numbers, Stated for ℝ §operations, $+$ and $\cdot$ are binary operations on the set $\mathbb{R}$ and $0\in\mathbb{R}$, so Associative and Commutative Binary Operations, and Neutral Elements applies to them with $X=\mathbb{R}$. By Arithmetic and Order Rules in the Real Numbers, Stated for ℝ §associative, $(u\cdot v)\cdot w=u\cdot(v\cdot w)$ for all $u,v,w\in\mathbb{R}$; this is the condition of Associative and Commutative Binary Operations, and Neutral Elements §associative for $\cdot$, which gives clause mul-associative. By Arithmetic and Order Rules in the Real Numbers, Stated for ℝ §commutative, $u\cdot v=v\cdot u$ for all $u,v\in\mathbb{R}$; this is the condition of Associative and Commutative Binary Operations, and Neutral Elements §commutative for $\cdot$, which gives clause mul-commutative. By Arithmetic and Order Rules in the Real Numbers, Stated for ℝ §neutral, $0+u=u$ and $u+0=u$ for every $u\in\mathbb{R}$; with $0\in\mathbb{R}$ this is the condition of Associative and Commutative Binary Operations, and Neutral Elements §neutral for $+$ and $e=0$, which gives clause add-neutral.

Clause strict. Let $x,y\in\mathbb{R}$. By the clause partial-order, $\le$ is a partial order on the set $\mathbb{R}$, and $<$ is its associated strict relation of Partial and Total Orders on a Set and the Associated Strict Relation §strict. By Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-characterization, applied to $\mathbb{R}$ and $\le$, $x<y$ holds if and only if $x\le y$ and $x\neq y$. So if $x<y$, then $x\le y$.

Clause sub-add. Let $x,y\in\mathbb{R}$. By Negatives, Differences, Reciprocals and Quotients §negative, applied to the commutative ring $\mathbb{R}$ of the clause field, $x-y=x+(-y)$, where $-y$ is the negative of $y$; and $-y\in\mathbb{R}$ by Arithmetic and Order Rules in the Real Numbers, Stated for ℝ §operations. Hence

$$(x-y)+y=(x+(-y))+y=x+((-y)+y)=x+0=x,$$

where the second equation is Arithmetic and Order Rules in the Real Numbers, Stated for ℝ §associative with $x$, $-y$ and $y$ in place of $x$, $y$ and $z$; the third is Arithmetic and Order Rules in the Real Numbers, Stated for ℝ §negative with $y$ in place of $x$, which gives $(-y)+y=0$; and the fourth is Arithmetic and Order Rules in the Real Numbers, Stated for ℝ §neutral, which gives $x+0=x$.

Clause square. Let $x\in\mathbb{R}$. By The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §digits and Arithmetic and Order of the Natural Numbers §digits, the digit $2$ is a natural number and $2=1+1$ in $\mathbb{N}_{0}$; and $1\in\mathbb{N}\subseteq\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets. Applying Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §exponents to the commutative ring $\mathbb{R}$ of the clause field, with $m=n=1$, gives $x^{2}=x^{1+1}=x^{1}\cdot x^{1}$; and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product, applied to the same commutative ring, gives $x^{1}=x$. Hence $x^{2}=x\cdot x$.