Floating point bitwise comparator. If f1 and f2 are floating point numbers with the following properties can we always say f1 > f2? Recall floating-point representation:
Suppose $f$ is a floating-point number then we can express f as,
If $f$ is normal:
$$(-1)^{s}\cdot2^{e-127}(1 + \sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k})$$
If $f$ is denormal/subnormal: $(e = 0)$
$$(-1)^{s}\cdot2^{-126}(0 + \sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k})$$
where

$s$ is the sign of $f$.
$e$ is the stored exponent of $f$. This means $e-127$ is the effective exponent of $f$.
$b_k$ is the $k$-th bit of $f$ where $b_0$ is the LSB and $b_{22}$ is the MSB.

Let $f_1$ be a floating-point number with constants $s_1, e_1,$ and $b_{1k}$.
Let $f_2$ be a floating-point number with constants $s_2, e_2,$ and $b_{2k}$.
I'm trying to find out if the following statement is true: $e_1 &gt; e_2 &gt; 0$ and $s_1 = s_1$ then $f_1 &gt; f_2$.
My initial strategy was to subtract $f_2$ from $f_1$ and show that it must be strictly greater than $0$.
What I have so far.
$
\begin{align*}
f_1-f_2 &amp;= 2^{e_1-127}(1 + \sum\limits_{k=1}^{23} b_{1,23-k}\cdot 2^{-k}) - 2^{e_2-127}(1 + \sum\limits_{k=1}^{23} b_{2,23-k}\cdot 2^{-k})\\
&amp;= 2^{-127}(2^{e_1}(1 + \sum\limits_{k=1}^{23} b_{1,23-k}\cdot 2^{-k}) - 2^{e_2}(1 + \sum\limits_{k=1}^{23} b_{2,23-k}\cdot 2^{-k})) \\
&amp;= 2^{-127}(2^{e_1} + \sum\limits_{k=1}^{23} b_{1,23-k}\cdot 2^{e_1-k} - 2^{e_2} - \sum\limits_{k=1}^{23} b_{2,23-k}\cdot 2^{e_2-k})\\
&amp;=2^{-127}(2^{e_1} - 2^{e_2} + \sum\limits_{k=1}^{23} b_{1,23-k}\cdot 2^{e_1-k} - \sum\limits_{k=1}^{23} b_{2,23-k}\cdot 2^{e_2-k})\\
&amp;=2^{-127}(2^{e_1} - 2^{e_2} + \sum\limits_{k=1}^{23}(b_{1,23-k}\cdot 2^{e_1-k}-b_{2,23-k}\cdot 2^{e_2-k}))
\end{align*}
$
Now since $e_1 &gt; e_2 \iff e_1-e_2 &gt; 0 \iff 2^{e_1}-2^{e_2} &gt; 1$ we have that:
$
\begin{align*}
f_1-f_2 &amp; &gt; 2^{-127}(1 + \sum\limits_{k=1}^{23}(b_{1,23-k}\cdot 2^{e_1-k}-b_{2,23-k}\cdot 2^{e_2-k}))
\end{align*}
$
In order for the above to always be greater than zero I require that $\sum\limits_{k=1}^{23}(b_{1,23-k}\cdot 2^{e_1-k}-b_{2,23-k}\cdot 2^{e_2-k}) &gt; -1$.
However, I don't know how to formally show this. Any help/hints are much appreciated as inequalities are not my strong suit.
If we study the expression for a floating point number, $$(-1)^{s}\cdot2^{e-127}(1 + \sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k}),$$
and pay attention to the sum $\sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k}$, we note that
$$0 \leq \sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k} \leq \sum\limits_{k=1}^{23} 2^{-k} &lt; \sum\limits_{k=1}^\infty 2^{-k} = 1,$$
where the last equality is formed by evaluating the geometric series. Thus we find that
$$2^{e-127} \leq2^{e-127}(1 + \sum\limits_{k=1}^{23} b_{23-k}\cdot 2^{-k}) &lt; 2^{e-127}\cdot 2$$
Thus if $s = 0$ and $e_1 &gt; e_2$ we find that $f_2 &lt; 2^{e_2 - 127} \cdot 2 \leq 2^{e_1 - 127} \leq f_1$.
Note that if $s = 1$ and $e_1 &gt; e_2$, the signs are reversed and we actually have $f_2 &gt; f_1$. But always $|f_1| &gt; |f_2|$.

The extended result of the above is that if we ignore the effects of denormal numbers, NaNs, infinities and say that $-0 &lt; 0$, we have
$$f_1 &lt; f_2 \iff n_1 &lt; n_2,$$
where $n_1, n_2$ are the bit patterns of $f_1, f_2$ interpreted as $w$-bit two's complement integers.