Let $t \mapsto \log t$ be the D865: Standard natural real logarithm function.
Let $x, y \in (0, \infty)$ each a D5407: Positive real number such that
Let $x, y \in (0, \infty)$ each a D5407: Positive real number such that
| (i) | \begin{equation} x < y \end{equation} |
Then
\begin{equation}
\log x < \log y
\end{equation}