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

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $a$, $b$, $c$ and $d$ be real numbers, read as elements of the type $\mathrm{Real}$ of The Real Numbers as a Type (i), with $0$, $1$, $+$, $\cdot$, $\le$ and $<$ those of $\mathrm{Real}$ (The Real Numbers as a Type (ii)). Reciprocals $c^{-1}$ and quotients $a/c$ are those of Negatives, Differences, Reciprocals and Quotients (ii), and absolute values $|a|$ those of Absolute Value in an Ordered Field (i), taken in $\mathbb{R}$ and read in $\mathrm{Real}$ as in Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (ii) and Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (iii), where, for $q$ in $\mathrm{Real}$ and a set $s$, $q=s$ means that the set of $q$ is $s$, as in Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real; $2=1+1$.

(i) Multiplying on the right. If $a\le b$ and $0\le c$, then $a\cdot c\le b\cdot c$.

(ii) Multiplying on the left. If $a\le b$ and $0\le c$, then $c\cdot a\le c\cdot b$.

(iii) Nonnegative products. If $0\le a$ and $0\le b$, then $0\le a\cdot b$.

(iv) Positive products. If $0<a$ and $0<b$, then $0<a\cdot b$.

(v) Multiplying inequalities. If $0\le a\le b$ and $0\le c\le d$, then $a\cdot c\le b\cdot d$.

(vi) Cancelling a positive factor. If $a\cdot c\le b\cdot c$ and $0<c$, then $a\le b$.

(vii) Reciprocals. If $c\neq0$, there is $y$ in $\mathrm{Real}$ with

$$c\cdot y=1,\qquad y=c^{-1}=1/c,$$

and if moreover $0<c$, then $0<y$.

(viii) Halves. There is $q$ in $\mathrm{Real}$ with $a=q+q$, namely $q=a/2$.

(ix) A positive number below two positive numbers. If $0<a$ and $0<b$, there is $c'$ in $\mathrm{Real}$ with $0<c'$, $c'\le a$ and $c'\le b$, namely $c'=a$ if $a\le b$ and $c'=b$ otherwise.

(x) Strict bounds on an absolute value.

$$|a|<c\iff -c<a\ \text{and}\ a<c .$$

(xi) Vanishing absolute value. $|a|=0$ if and only if $a=0$.

(xii) A number lies between $\pm$ its absolute value. $-|a|\le a\le|a|$.