Proof of Order Rules for Products, Halves, Minima and Absolute Values in ℝ

Throughout, $\mathbb{R}$ is an ordered field by The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (i), so the rules of Rules of Arithmetic and Order in an Ordered Field and Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares apply to it; most clauses are these published ordered-field rules read in the type $\mathrm{Real}$, whose elements are determined by their sets (The Real Numbers as a Type (i)) and whose order is total (The Real Numbers as a Type (v)).

Products. (i) is Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (v), and (ii) follows by commutativity. (iii) and (iv) are Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (iv). For (v), $0\le b$ since $0\le a\le b$, and

$$a\cdot c\le b\cdot c\le b\cdot d$$

by (i) and (ii). (vi) is the converse direction of Rules of Arithmetic and Order in an Ordered Field (vi).

Reciprocals and halves. Let $c\neq0$. By Negatives, Reciprocals and the Strict Order in an Ordered Field, as Values (ii), $c^{-1}\in\mathbb{R}$ and $c\cdot c^{-1}=1$; let $y$ be the element of $\mathrm{Real}$ whose set is $c^{-1}$. Then $c\cdot y=1$, and $c^{-1}=1/c$ by The Quotient 1/x, Order Rules for Sums, and Nesting of Closed Intervals in ℝ (i). If $0<c$, then $0<c^{-1}$ by Rules of Arithmetic and Order in an Ordered Field (viii). This proves (vii). For (viii): $0<2$ by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (vii), so $2\neq0$, and by Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (ii) there is $q$ in $\mathrm{Real}$ with $q=a/2$ and $q\cdot2=a$. Hence

$$q+q=q\cdot1+q\cdot1=q\cdot(1+1)=a .$$

Minima. For (ix): if $a\le b$, then $c'=a$ satisfies $0<c'$, $c'\le a$ and $c'\le b$; otherwise $b\le a$ by totality, and $c'=b$ satisfies $0<c'$, $c'\le a$ and $c'\le b$.

Absolute values. (xi) and (xii) are part of Rules of Arithmetic and Order in an Ordered Field (x), and (x) is Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (ix).