I've just happened to read this question on MO (that of course has been closed) and some of the answers to a similar question on MSE.
I know almost nothing of nonstandard analysis and was asking myself if something like the sentence « $1- 0.999 \dots$ is a nonzero positive infinitesimal» could be easily expressed and proved in nonstandard analysis.
First of all, what is 0.999… ? If we take the usual definition as a series or as a limit of a sequence of rationals, then it will still be a real number and equal to $1$ (I guess by "transfer principle", but please correct me if I'm wrong).
Instead, let's define
$$0.9_N:=\sum_{i=1}^N 9\cdot 10^{-i} $$
where $N\in{}^*\mathbb{N}\setminus\mathbb{N}$ is an infinite nonstandard natural number. This $0.9_N$ is a legitimate element of ${}^*\mathbb{R}$, expressed as $0.$ followed by an infinite number of "$9$" digits.
What can be said about $\epsilon_N:=1-0.9_N$ ? Is there an elementary proof that $\epsilon_N$ is a positive infinitesimal of ${}^*\mathbb{R}$ ? (by "elementary" I mean just order and field axioms and the intuitive facts about infinitesimals, like that for $x$ infinite $1/x$ is infinitesimal etc.; no nonprincipal ultrafilters & C).
Best Answer
We can use the geometric series formula:
$$0.9_N = \sum_{i=1}^N 9 \cdot 10^{-i} = 9 \cdot 10^{-1} \cdot \frac{1 - 10^{-N}}{1 - 10^{-1}} = (1 - 10^{-N})$$
Since $N$ is infinite, $\epsilon_N = 10^{-N} = 1 / 10^N$ is infinitesimal.