If $\ln x$ is defined via an integral and $e$ defined from $\ln x$, how would you prove that $\ln x$ is the inverse of $e^x$? This is a somewhat technically specific question about the relationship between $\ln x$ and $e^x$ given one possible definition of $\ln x$.
Suppose that you define $\ln x$ as
$$\ln x = \int_1^x{\frac{dt}{t}}$$
We can use the connection between the integral definition of $\ln x$ and the harmonic series to show that $\ln x$ grows unboundedly. This function is monotonically increasing, so it should have an inverse mapping from its codomain ($\mathbb{R}$) to its domain ($\mathbb{R^+}$). Let's call that function $\ln^{-1} x$.
Since $\ln x$ grows unboundedly and is zero when $x$ is $1$, we can define $e$ as the unique value such that $\ln e = 1$.
So here's my question: given these starting assumptions, how would you prove that $\ln^{-1} x = e^x$ (or, equivalently, that $\ln x = \log_e x$? I'm having a lot of trouble even seeing how you'd get started proving these facts, since basically every calculus fact I know about $e$ and $\ln x$ presumes this result to be true.
Thanks!
 A: If $f(x)=\log x$ is defined as a primitive of $\frac{1}{x}$ for which $f(1)=0$, then $f(ab)=f(a)+f(b)$ holds for any couple of positive real numbers. This gives that the inverse function $g(x)$ is a $C^1$ function, satisfies $g(0)=1$ and the functional equation:
$$ g(a)g(b)=g(a+b)\tag{1} $$
for any couple of real numbers $a,b$. $(1)$ and differentiability grants that $g'=g$, hence $g(x)=e^x$.
A: There have been several questions on definition of $\log x$ and $e^{x}$ and the general power $a^{x}$. Some links are available in various comments on the question. I strongly believe that the real confusion arises because most introductory textbooks on calculus (designed to be consumed by students of 16-17 years of age) don't define any of these functions. They just introduce it with a list of their properties and provide some standard limit formulas. For the benefit of students who are frustrated by such books I have a series of blog posts starting with this one.
The current question defines $\log x$ as an integral and says that $\log e = 1$ and $\log x$ possesses an inverse which is a map from $\mathbb{R}$ to $\mathbb{R}^{+}$. This part is correctly understood by OP. Now the question is how to show that this inverse map is same as $e^{x}, x\in \mathbb{R}$. From the wording of the question it is clear that OP is aware of some definition of $e^{x}$ (although not mentioned in the question) and OP wants to identify it as the inverse of $\log x$. Based on various definitions of $e^{x}$ it is possible to do so (as done in my blog posts). However a nice approach could be to define the expression $e^{x}$ directly as the inverse of $\log x$.
In case one desires to have an independent definition of $e^{x}$ say $e^{x} = \lim_{n \to \infty}(1 + (x/n))^{n}$ then we can show using this definition that $e^{x}$ possesses an inverse and derivative of $y = e^{x}$ is again $y = e^{x}$ so that $dx/dy = 1/y$ and hence $x$ can be defined as the integral $\int (dy/y)$. This way we can identity the inverse of $e^{x}$ with the $\log $ defined as an integral. Same can be done if we define $e^{x}$ as $$e^{x} = 1 + x + \frac{x^{2}}{2!} + \frac{x^{3}}{3!} + \cdots$$
In any systematic theory of $\log x, e^{x}, a^{x}$ it is sufficient (and perhaps pedagogically better) to define any one of these symbols and develop the rest on the basis of the definition. For example when we start with defining $\log x$ as integral we can define $e^{x}$ as the inverse and $a^{x} = e^{x\log a}$.
A: The advantage of defining $\ln x$ as an integral is that it gives a simple way to define $e^x$ in elementary calculus (without resorting to infinite series, taking limits of rational powers of $e$, or other methods).
Once $\ln x$ has been defined in this way, you can establish that $y=\ln x$ is an increasing function whose range is $\mathbb{R}$, so it has an inverse function with domain $\mathbb{R}$ which we can $\mathbf{define}$ to be $y=e^x$.
With this definition, we have the identities 
$\ln(e^x)=x$ for all $x$ and $e^{\ln x}=x$ for $x>0$, and  $\ln e=1\implies e^{1}=e$.
