In self-studying a textbook on computability theory, I found that many of the exercises depend on the following factlet:
A dyadic rational is a rational number whose denominator is a power of two, i.e. a rational number of the form $\frac{a}{2^b}$. A real number is a dyadic rational if and only if its binary expansion terminates.
I have the following for the forward direction:
The binary expansion of a number between $0$ and $1$ is of the form \begin{equation*} 0.x_1x_2x_3\cdots = \sum_{k=1}^{\infty}x_k2^{-k} = \sum_{k=1}^{\infty}\frac{x_k}{2^k} \end{equation*} Suppose a number $0 < x < 1$ has a terminating binary expansion. Then its expansion is of the form $0.x_1\cdots x_k$, where $x_k$ is the last $1$ digit. Then \begin{equation*} x = \frac{x_1}{2^1} + \frac{x_2}{2^2} + \ldots + \frac{x_k}{2^k} = \frac{x_12^{k-1} + x_22^{k-2} + \ldots + x_k}{2^k} \end{equation*} Since this is base-$2$, each $x_i$ must be either $0$ or $1$, whence it follows that the denominator and numerator are integers, and the denominator is a power of two, which means $x$ is a dyadic rational.
For the converse, I have the following idea, but do not have the background to write up a rigorous proof (in particular, I cannot imagine how to deal with the ambiguity of infinite $1$s versus infinite $0$s at some point in the expansion):
Conversely, we must show that if $0 < \frac{a}{2^b} < 1$ is a dyadic rational, then its binary expansion terminates. Every dyadic rational can be represented as the finite sum/product $\left(\frac{1}{2} + \ldots + \frac{1}{2}\right)\frac{1}{2}\cdot\ldots\cdot\frac{1}{2}$. The binary expansion of the sum of two numbers with terminating binary expansions terminates, same for the product; and it follows that the binary expansion of a dyadic rational terminates.
I have not yet formally tackled (but have vague, possibly incorrect, intuition of) the construction of real numbers, Cauchy convergence and proof by induction (which I gather could be used somehow...), but I need to convince myself of the factlet and its possible pitfalls to continue with the material for the time being (namely, Cantor's diagonalization proofs). Any detailed hints or full-on proofs would be greatly appreciated.
(I have found this question but the hint in the answer seems unhelpful given my lack of background.)
EDIT:
Observe that $a$ is a finite integer, and so can be written as the finite-term sum $x_12^{k-1} + x_22^{k-2} + \ldots + x_k$, where $x_i \in \{0, 1\}$. Since $\frac{a}{2^b} < 1$, it follows that $a < 2^b$. By the definition of binary expansion, $x_1 = 1$, whence $2^{k-1} \le a < 2^b$, and we have $k-1<b$. But $1 \le i \le k$, whence $k-i<b$. Then we can divide each term by $2^b$, obtaining: \begin{equation*} \frac{a}{2^b} = \frac{x_1}{2^{b-k+1}} + \frac{x_2}{2^{b-k+2}} + \ldots + \frac{x_k}{2^b}, \end{equation*} which gives us a finite binary expansion; this completes the proof.
