Proof of Differences, Quotients and Absolute Values of Real Numbers, Read in the Type Real

By The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (ii), $\mathbb{R}$ is an ordered field, so the results on ordered fields cited below apply to it. By The Real Numbers as a Type (ii), the sums, products, negatives and order of $\mathrm{Real}$ are those of $\mathbb{R}$, and an element of $\mathrm{Real}$ is determined by its set (The Real Numbers as a Type (i)); so each equation below, proved in $\mathbb{R}$, holds in $\mathrm{Real}$.

(i): By Negatives, Differences, Reciprocals and Quotients (i), $-y$ is the unique element of $\mathbb{R}$ with $y+(-y)=0$, and $x-y$ is by definition $x+(-y)$. The negative $-y$ of $\mathrm{Real}$ is this same element and the difference of $\mathrm{Real}$ is $x+(-y)$ (The Real Numbers as a Type (ii)), so the two differences agree. $x-y\in\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima (i).

(ii): Let $y\neq0$. $x/y\in\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima (ii), and $x/y=x\cdot y^{-1}$ and $(x/y)\cdot y=x$ by Difference and Quotient Identities in ℝ (ii).

(iii): $|x|\in\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima (iii). By Absolute Value in an Ordered Field (i), $|x|=x$ if $0\le x$ and $|x|=-x$ otherwise; if $x<0$ then $0\le x$ fails by Negatives, Reciprocals and the Strict Order in an Ordered Field, as Values (iii), so $|x|=-x$. $0\le|x|$ by Rules of Arithmetic and Order in an Ordered Field (x). Finally, $u=x-y$ lies in $\mathbb{R}$ by (i), $-(x-y)=y-x$ by Difference and Quotient Identities in ℝ (i), and $|-u|=|u|$ by Rules of Arithmetic and Order in an Ordered Field (x); hence $|y-x|=|-(x-y)|=|x-y|$.