Proof of Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real

Sketch. 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), an element of $\mathrm{Real}$ is determined by its set (The Real Numbers as a Type (i)), and the arithmetic in $\mathrm{Real}$ below uses only the laws of $\mathrm{Real}$ in The Real Numbers as a Type: those of a commutative ring (The Real Numbers as a Type (iv)), of its total order (The Real Numbers as a Type (v)) and of an ordered ring (The Real Numbers as a Type (vi)).

For (i): the difference of $x$ and $y$ in $\mathbb{R}$ is $x+(-y)$ by Negatives, Differences, Reciprocals and Quotients (i), and this is the set of $x-y$ in $\mathrm{Real}$ by The Real Numbers as a Type (ii); in particular it lies in $\mathbb{R}$.

For (ii): by Negatives, Reciprocals and the Strict Order in an Ordered Field, as Values (ii), $y^{-1}\in\mathbb{R}$ and $y\cdot y^{-1}=1$, so $y^{-1}$ is the set of an element $r$ of $\mathrm{Real}$ with $y\cdot r=1$. By Negatives, Differences, Reciprocals and Quotients (ii), $x/y=x\cdot y^{-1}$, which is the set of $x\cdot r$; hence $x/y\in\mathbb{R}$, $q=x/y$ for $q=x\cdot r$, and

$$q=x/y\iff q=x\cdot r\iff q\cdot y=x,$$

the second step because $y\cdot r=1$ (multiply by $y$, respectively by $r$).

For (iii): by Absolute Value in an Ordered Field (i), $|x|=x$ if $0\le x$ and $|x|=-x$ otherwise; both lie in $\mathbb{R}$. So if $q=|x|$, then either $0\le x$ and $q=x$, or $x<0$ (by totality of $\le$) and $q=-x$; in both cases $0\le q$. Finally $y-x=-(x-y)$ in $\mathrm{Real}$, so the set of $y-x$ is the negative in $\mathbb{R}$ of the set of $x-y$ (The Real Numbers as a Type (ii)), and $|y-x|=|-(x-y)|=|x-y|$ by Rules of Arithmetic and Order in an Ordered Field (x).

For (iv): in $\mathbb{R}$,

$$|-x|=|x|,\qquad |x\cdot y|=|x|\cdot|y|,\qquad |x|\le c\iff -c\le x\le c$$

by Rules of Arithmetic and Order in an Ordered Field (x), and $|x+y|\le|x|+|y|$ by Rules of Arithmetic and Order in an Ordered Field (xi). By The Real Numbers as a Type (ii), negatives, sums, products and the order of $\mathbb{R}$ are those of $\mathrm{Real}$, read on sets. So if $p=|-x|$ and $q=|x|$, then $p$ and $q$ have the same set, and $p=q$. If $p=|x|$ and $q=|y|$, then the set of $p\cdot q$ is $|x|\cdot|y|=|x\cdot y|$, so $r=|x\cdot y|$ gives $r=p\cdot q$; and the set of $p+q$ is $|x|+|y|\ge|x+y|$, so $r=|x+y|$ gives $r\le p+q$. If $q=|x|$, then $q\le c$ in $\mathrm{Real}$ means $|x|\le c$ in $\mathbb{R}$, that is, $-c\le x$ and $x\le c$ in $\mathbb{R}$, and so in $\mathrm{Real}$.

For (v): as $x,y\in\mathbb{R}$, neither $x=-\infty$ nor $y=\infty$ (The Extended Real Line, Its Order, and [0,∞] (i)), so by The Extended Real Line, Its Order, and [0,∞] (iii) $x\le y$ in $[-\infty,\infty]$ if and only if $x\le y$ in $\mathbb{R}$, that is, in $\mathrm{Real}$. In $[-\infty,\infty]$, $x<y$ means $x\le y$ and $x\neq y$; by the first part and antisymmetry of $\le$ on $\mathrm{Real}$, this holds exactly when $x\le y$ and not $y\le x$ in $\mathrm{Real}$, that is, when $x<y$ in $\mathrm{Real}$. Finally $-\infty\le x\le\infty$ by The Extended Real Line, Its Order, and [0,∞] (iii), and $x\neq\pm\infty$ as $\pm\infty\notin\mathbb{R}$.