Let $\log$ be the D865: Standard natural real logarithm function.
Let $a \in (0, \infty)$ be a D5407: Positive real number.
Let $a \in (0, \infty)$ be a D5407: Positive real number.
Then
\begin{equation}
\lim_{x \searrow 0, \, x \neq 0} \frac{a^x - 1}{x}
= \log a
\end{equation}