How do I prove that every hyperreal has a standard part after constructing the reals from the hyperrationals? In texts on nonstandard analysis, I've come across references to the following construction of the real numbers: starting from the hyperrationals $^*\mathbb Q$, say that $\mathbb R$ is the quotient ring of the maximal ideal $\mathrm{mon}_{^*\mathbb Q}(0)$ in the subring $\mathrm{gal}_{^*\mathbb Q}(0)$, where:


*

*$\mathrm{gal}_{^*\mathbb Q}(0)$ is the galaxy in $^*\mathbb Q$ of 0, i.e. the set of the finite hyperrationals,

*$\mathrm{mon}_{^*\mathbb Q}(0)$ is the monad in $^*\mathbb Q$ of 0, i.e. the set of the infinitesimal hyperrationals.


(Note: the order is defined by $\mathrm{mon}_{^*\mathbb Q}(x) < \mathrm{mon}_{^*\mathbb Q}(y)$ iff $x < y$ and $x \approx y$, for every pair of hyperrationals $x, y$. This works because $\mathrm{mon}_{^*\mathbb Q}(x)$ is an interval: hyperrationals between infinitesimals are also infinitesimal.)
This construction seems to me to be the most natural one in a context where the tools of nonstandard analysis are being utilized. However the expositions I've read were too cursory/generalized/confusing, so I've been trying to work out the details myself. In particular I've been having some trouble with proving completeness.
I can prove, using this construction, that the reals are Dedekind and Cauchy complete, i.e. every nonempty upper-bounded set of reals has a supremum and every Cauchy sequence in $\mathbb R$ is convergent. However, there is a third formulation of the completeness of $\mathbb R$ which seems like the natural formulation given the construction described above (just as Dedekind completeness is the natural formulation given the Dedekind cut construction and Cauchy completeness is the natural formulation given the Cauchy sequence construction). Namely, the standard part principle—“every finite hyperreal number is infinitely close to a real number”.
I can prove the standard part principle from Dedekind or Cauchy completeness. But surely there is some way to prove it directly from the construction described above, without going to the trouble of proving Dedekind or Cauchy completeness. My proofs also have the issue that they are basically standard analysis proofs, rather than nonstandard analysis proofs. I'm used to standard analysis, so I find it much easier to think that way. So there may be a very simple nonstandard analytic argument I haven't thought of.
I can get this far:
Lemma 1. $\mathbb R$ is Archimedean.
Proof. Suppose $x$ is a real number. Let $r \in x$, so that $r$ is a finite hyperrational. Then there is a rational $a \ge r$. Because $\mathbb Q$ is Archimedean, there is an integer $n \ge a$. Because $r \le a \le n$, we have $\mathrm{mon}_{^*\mathbb Q}(r) \le \mathrm{mon}_{^*\mathbb Q}(n)$ (where $\le$ is the order in $\mathbb R$), and because $\mathrm{mon}_{^*\mathbb Q}(1)$ is the multiplicative identity in $\mathbb R$, the real number
\begin{equation*}
\mathrm{mon}_{^*\mathbb Q}(n) = \underbrace{\mathrm{mon}_{^*\mathbb Q}(1) + \dotsb + \mathrm{mon}_{^*\mathbb Q}(1)}_{n \text{ times}}
\end{equation*}
is an integer in $\mathbb R$.
Lemma 2. $\mathbb Q$ is dense in $\mathbb R$, i.e. every hyperreal number is infinitely close to a hyperrational number.
Proof. Suppose $x$ is a hyperreal number. Let $n$ be a large hyperinteger. Because $\mathbb R$ is Archimedean, by transfer, there is a hyperinteger $m \ge nx$. Let $m$ be the least such hyperinteger. Then $x - m/n = (nx - m)/n < 1/n$ is infinitesimal.
Theorem. $\mathbb R$ has the standard part property.
Proof. Suppose $x$ is a finite hyperreal. By Lemma 2 there is a hyperrational $r \approx x$. Because $x$ is finite, so is $r$. Let $a = \mathrm{mon}_{^*\mathbb Q}(r)$. Then $a$ is a real number…
If I could prove that $a$ in the above proof was infinitely close to $r$, I'd be done. It seems, intuitively, like every hyperrational number should be infinitely close (in $^*\mathbb R$) to the real number identified with its monad, but I don't know how to prove this or even really how to approach the problem.
(By the way, I've been working in a axiomatic nonstandard analysis framework where a $^*$-map and the transfer and saturation principles are taken as given, so ideally I'd like a solution that relies on these axioms rather than  a specific ultrafilter construction. But I'd still be interested in any solution.)
 A: To specify a standard part function defined on all finite hyperrationals, use Dedekind cuts.  Namely, to each finite hyperrational one associates a Dedekind cut on $\mathbb Q$ as follows.  
If the hyperrational is infinitely close to a rational, then the cut is simply the cut defined by that rational.  
Therefore we can assume that the hyperrational $\alpha$ is not infinitely close to a rational.  Then we consider the partition of $\mathbb Q$ into complementary sets $L_\alpha=\{x\in\mathbb Q\colon x\leq\alpha\}$ and similarly $R_\alpha=\{x\in\mathbb Q\colon x>\alpha\}$.  The real number defined by that Dedekind cut is the standard part of $\alpha$.
Note that completeness is equivalent to the existence of a standard part function.
A: I did find an answer to my question on my own eventually (i.e. to prove that every finite hyperrational number is infinitely close to a real number directly from the construction of $\mathbb R$ as a quotient of ${}^*\mathbb Q$, without having to deal with Dedekind cuts or Cauchy sequences).
The only thing I had left to prove was that every finite hyperrational number is infinitely close to the real number corresponding to its monad. Let $E$ be the epimorphism from $\mathrm{gal}_{{}^*\mathbb Q}(0)$ to $\mathbb R$, which when restricted to $\mathbb Q$ is a monomorphism. Then the problem is to prove that for every finite hyperrational number $x$, we have $x \approx E(x)$. Now, $E$ is order-preserving (because by the definition of the order in the quotient, we have $E(x) < E(y)$ iff $x < y$ and $x \not \approx y$). So for every pair of rationals $r$ and $s$ such that $r < E(x) < s$, i.e. $E(r) < E(x) < E(s)$ (since we can identify rational numbers with their values under $E$), we have $r < x < s$. So, $x$ is between the rational numbers less than $E(x)$ and the rational numbers greater than $E(x)$. Intuitively it follows that $x \approx E(x)$, although proving it turned out to be more complicated than expected. I had to use the following lemma:
Lemma. A finite hyperrational can be approximated to arbitrarily small rational error by rationals, on both sides.
Proof. Suppose $x$ is a finite hyperrational and $\varepsilon \in \mathbb Q$ is positive. Then there are rationals $a$ and $b$ such that $a < x < b$. Let $n$ be an integer greater than $(b - a)/\varepsilon$, so that $(b - a)/n < \varepsilon$, and consider the partition given by
\begin{equation*}
c_k = a + k \frac {b - a} n,
\end{equation*}
for $k \in \{0, \dotsc, n\}$. We have $c_0 = a < x < b$, so there is an $i$ such that $c_i < x$ and a $j$ such that $c_j > x$. Choose $i$ as large as possible and $j$ as small as possible. Then $c_{j - 1} \le x \le c_{i + 1}$, so
\begin{align*}
x - \varepsilon < c_{i + 1} - \frac {b - a} n = c_i < x < c_j = c_{j - 1} + \frac {b - a} n < x + \varepsilon,
\end{align*}
and $c_i$ and $c_j$ are rational.
Using the lemma, I could prove that the condition described above did imply $x$ and $E(x)$ were infinitely close.
Theorem. For every finite hyperrational $x$ and every hyperrational $y$, if, for any two rationals $r$ and $s$ such that $r < x < s$, we have $r < y < s$, then $x \approx y$.
Proof. Suppose $x$ is a finite hyperrational, $y$ is a hyperrational and for any two rationals $r$ and $s$ such that $r < x < s$, we have $r < y < s$; and suppose $\varepsilon \in \mathbb Q$ is positive. Then by Lemma 1 we have rationals $r$ and $s$ such that $x - \varepsilon < r < x < s < x + \varepsilon$. Because $r < x < s$, we have $r < y < s$, hence $x - \varepsilon < r < y < s < x + \varepsilon$, hence $|x - y| < \varepsilon$.
