Proof of Comparison of Real Numbers with Arbitrary Positive Slack

Conventions. The order $\le$, its associated strict order $<$, and the arithmetic of $\mathbb{R}$ are those of the ordered field of real numbers; in particular $\le$ is a total order, so it is antisymmetric and, for any two real numbers, one is at least the other. Among the ordered field axioms is the compatibility of $\le$ with addition: if $a\le b$ then $a+c\le b+c$ for every $c\in\mathbb{R}$. That axiom is what we use for non-strict inequalities; claim 1 of Elementary Order Arithmetic in an Ordered Field is its strict counterpart and is cited only where the inequality is strict.

Claim 1. Assume $a\le b+\varepsilon$ for every positive $\varepsilon\in\mathbb{R}$, and suppose that $a\le b$ fails. By the totality of $\le$ we then have $b\le a$ and $b\ne a$, that is, $b<a$. By claim 1 of Elementary Order Arithmetic in an Ordered Field, adding $-b$ to both sides gives $0<a-b$, so claim 8 there shows that

$$\varepsilon_{0}=(a-b)\cdot2^{-1}$$

is positive and satisfies $\varepsilon_{0}<a-b$. The hypothesis applied with $\varepsilon_{0}$ gives $a\le b+\varepsilon_{0}$, and adding $-b$ to both sides gives $a-b\le\varepsilon_{0}$ by the compatibility of $\le$ with addition. Combining with $\varepsilon_{0}<a-b$ by claim 2 of that lemma yields $a-b<a-b$, which is impossible since $<$ requires the two sides to be distinct. Hence $a\le b$.

Claim 2. Assume $b-\varepsilon\le a$ for every positive $\varepsilon\in\mathbb{R}$. Fix such an $\varepsilon$; adding $\varepsilon$ to both sides of $b-\varepsilon\le a$, which the compatibility of $\le$ with addition recorded in the Conventions permits, gives $b\le a+\varepsilon$, since $(b-\varepsilon)+\varepsilon=b$. As $\varepsilon$ was an arbitrary positive number, claim 1, applied with $b$ in the role of $a$ and $a$ in the role of $b$, gives $b\le a$.

Claim 3. Assume $0\le a$ and $a\le\varepsilon$ for every positive $\varepsilon\in\mathbb{R}$. Since $0+\varepsilon=\varepsilon$, the hypothesis reads $a\le0+\varepsilon$ for every positive $\varepsilon$, so claim 1, applied with $0$ in the role of $b$, gives $a\le0$. Together with $0\le a$ and the antisymmetry of the total order $\le$, this gives $a=0$.