Derivatives of Exponential Functions II

Earlier I presented a proof of the fomula for the derivative of the exponential function $f(x)=a^x$, i.e., $f'(x_0)=\ln(a)\cdot a^{x_0}$. The natural logarithm $\ln(a)$ was taken to be defined as the antidrivative of the function $\frac{1}{a}$. Here I show a different approach, in which $\ln(x)$ is taken to be defined as the inverse of the natural exponential, $e^x$. This implies that $e^{\ln(a)}=a$. The power function can then be rewritten as \begin{align} f(x) &= a^x = e^{\ln(a)\cdot x}\,. \end{align} Using the chain rule, \begin{align} f'(x) &= \ln(a)\cdot e^{\ln(a)\cdot x} = \ln(a)\cdot a^{x}\,, \end{align} recovering the earlier formula. From this and the earlier proof of the same formula, it follows that the two definitions of $\ln(a)$ must be equivalent, i.e. the inverse function of the natural exponential function is an antiderivative to the function $\frac{1}{a}$: \begin{align} g(a) &= e^a \quad \Leftrightarrow \quad g^{-1}(a)=\int \frac{1}{a}\,\mathrm{d}a \equiv \ln(a)\,. \end{align}