Finite binary representation of float number

Question

How can I prove that float number $x$ has the finite binary representation if and only if it is written like that: $ x = m / 2^n $, where $m, n \in \mathbb N$.

Should I consider something like 3 different cases for this format or can I do this in different way?

Thank you.

Answer 1

Here is a proof for positive rational numbers:

---

Let $x=\dfrac{m}{2^n}$ where $m,n\in\mathbb{N}$

Then $x=a+\dfrac{b}{2^n}$ where $a,b,n\in\mathbb{N}$ and $b<2^n$

Then length of the binary representation of $x$ is $\lceil\log_2(a+1)\rceil+n$

---

Let $a\in\mathbb{N}$ be the binary representation of the integer part of $x\in\mathbb{Q}$

Let $b\in\mathbb{N}$ be the binary representation of the fraction part of $x\in\mathbb{Q}$

Then $x=a+\frac{b}{2^{|b|}}=\frac{m}{2^n}$ where $m=a\cdot2^{|b|}+b,n=|b|\in\mathbb{N}$