Decimal expression of reals Let $x>0$ be real. Then $A_1=\{n\in \mathbb{N}\mid x<n\}$ is nonempty since $\mathbb{R}$ is dedekind complete. Since $\mathbb{N}$ is well ordered, $A_1$ has a least element $k$. Thus $k-1$ is the largest element of $A_2=\{n\in \mathbb{Z}\mid n\leq x\}$.
Thus for every $0<x\in \mathbb{R}$, there exists a largest integer $n\in \mathbb{Z}$ such that $n\leq x$.
Let $n_0$ be the largest integer such that $n_0\leq x$. If $n_0<x$, $10(x-n_0)>0$. Let $n_1$ be the largest integer less than or equal to this element. If I continue this process, i get $x=n_0 + n_1/10 + \cdots$
I don't know how to legitimate this process, since I can define finite decimals for this method but can't define infinite decimals. I think the existence of all the $n_k$'s should be guaranteed simultaneously, but don't know how..
 A: You can, indeed, define that recursively as you've begun. You've certainly got the general idea down, starting with $n_0$ as you've done. To pass to recursion, if we've got $n_0,...,n_k$, then let $n_{k+1}$ be the greatest integer $n$ such that $$n\leq 10^{k+1}\left(x-\sum_{j=0}^kn_j10^{-j}\right).$$ This is enough to prove existence. Of course, we don't have uniqueness ($1=0.9999...$), but this is a well-defined recursive algorithm to give you what you want.
Edit: I missed a rather large issue, here. Note that $n_0$ as defined above need not be a decimal digit, and can in fact be any nonnegative integer! All the others will end up being decimal digits, as it turns out, so this recursion takes care of all the decimal places to the right of the decimal point, but not those to the left.
As a fix, do it this way, instead. Note that the set $\{10^m:m\in\Bbb Z\}$ is unbounded. Thus, by similar reasoning to what you used, there is some greatest $m\in\Bbb Z$ such that $10^m\leq x$. Then $x<10^{m+1}$, so $10^{-m}x<10$, and let $n_m$ be the greatest integer $n$ such that $n\leq 10^{-m}x$--so of necessity, we will have $0\leq n_m\leq 9$, since $0<10^{-m}x<10$.
Now, for the recursion, suppose we've just defined $n_k$. Take $n_{k-1}$ to be the greatest integer $n$ such that $$10^{k-1}n\leq x-\sum_{j=k}^mn_j10^j.$$
You'll need to show that for all $k\leq m$, we have $0\leq n_k\leq 9$ (a fairly simple induction from $m$ toward $-\infty$, with the $k=m$ case holding as noted above), and that $$x=\sum_{j=-\infty}^mn_j10^j.$$ Note that we are now matching $n_j$ with $10^j$, rather than $10^{-j}$. You can alter this if you like, though the notation will become a bit more complicated.
A: From your work I think you will be able to formalize this much:

For every $i\in\mathbb{N}$ and $x\in\mathbb{R}$ and $y\leq x$, there exists a digit $0\leq d<10$ such that $x\in [y+d\cdot 10^i,y+(d+1)\cdot10^{i})$.

Note that this says $x-y\leq 10^{i+1}$.
Establish that there is a $k\in\mathbb{N}$ such that $10^k\leq x<10^{k+1}$. Set $x_0=x$ and  find $d_0$ where $x_0-d_010^k<10^{k+1}$. Inductively define $x_{i+1}:=x_{i}-d_i10^{k-i}$ where $d_i$ is a digit, ensuring $x_{i+1}<10^{k-i+1}$ as discussed above. Now define the series $s=\sum_{i=0}^\infty d_i10^{k-i}$. The only thing left to show is that $s$ actually converges to $x$.
By definition, $x-\sum_{i=0}^nd_i10^{k-i}=x_n-d_n10^{k-n}<10^{k-n+1}$. Since this is true for any $n$, the parital sums converge to $x$, and so $\sum_{i=0}^\infty d_i10^{k-i}$ is a decimal representation of $x$.
There is no doubt, an easier way and perhaps I overlooked something crass... but I enjoyed giving it a shot for the first time.
