I am trying to put together a more rigorous view of logarithms and exponentials than what is typically taught in a first-year calculus course. I know that we can define
$$\ln(x) = \int_{1}^x \frac{1}{t}dt,$$
and we can use this to show that this function satisfies the usual properties for logarithms, but does that mean it IS a logarithm?
Other approaches I have seen show that $\ln(x)$ is invertible, and define its inverse to be $e^x$, but this seems to raise the same question. Since we can prove that
$$e= \lim\limits_{n\to\infty} \left(1+\frac{1}{n}\right)^n,$$
using the integral definition of $\ln(x)$, it seems unwise to take this as a definition for $e$ and use that to argue that $\ln(x)$ is a logarithm.
Does anyone know of compatible definitions for $e$ and $\ln(x)$ that allow us to prove that $\ln(x)$ is a logarithm and that $e^x$ is its inverse without becoming circular? For example, can one use the integral definition to find a change of base formula for logs? Can you use this definition to show that $e^{\ln(x)}= x$?
Maybe it helps to change notation. Define $L(x) = \displaystyle \int_1^x \frac 1t \, dt$. It is fairly routine to show that $L$ is differentiable, increasing, and maps $(0,\infty)$ onto $(-\infty,\infty)$. Thus $L$ has a differentiable inverse $L^{-1}$ that is increasing and maps $(-\infty,\infty)$ onto $(0,\infty)$. Define $E(x) = L^{-1}(x)$.
It follows that $E(L(x)) = x$ for all $x > 0$ and $L(E(x)) = x$ for all $x \in \mathbb R$.
Using the inverse function theorem you find that $E'(x) = \dfrac{1}{L'(E(x))} = E(x)$.
The change-of-variable theorem implies that $L(x^n) = nL(x)$ for all $x > 0$ and natural numbers $n$. Since $$ \frac{n}{n+x} \frac xn \le \int_1^{1+x/n} \frac 1t \, dt \le \frac xn$$ for all such $x$ and $n$ you get $$\frac{nx}{n+x} \le nL(1+x/n) \le x$$ so that $$\lim_{n \to \infty} L \left( \left(1+\frac xn\right)^n \right) = x.$$ Since $E$ and $L$ are both continuous you conclude that $(1+x/n)^n$ converges as $n \to \infty$ and moreover $$E(x) = \lim_{n \to \infty} \left( 1 + \frac xn \right)^n.$$
The computation needs to be adjusted slightly if $x < 0$ but the limit remains valid for all $x$.