Inverse of the natural log function $y =\ln x$ Of course, it is a well known fact that the inverse of $y=\ln x$ (natural logarithm of x) is $e^x$. 
Assuming we haven't heard of the exponential function at all, how do we prove that the inverse of $\ln x$ i.e ($\ln^{-1} x$ ) is some other function, which indeed is the so called exponential function $e^x$? 

Let me be a little more concrete. If $y = \ln x$, then $x= A^y$, how do I prove that $A= e$?

There's another method by which I tried to arrive at the inverse of natural logarithm of $x$. 
By a theorem of differentiation of inverse functions
$$\left.\dfrac{df}{dx}\right|_{x=a} \cdot\left.\dfrac{df^{-1}}{dx}\right|_{x=f(a)}=1$$ 
I got an equation which looked like
$$\left.\dfrac{dF(x)}{dx}\right|_{x=\ln k}=k$$  where $k$ is a real number. 
How do I actually show that $F(x)$ is that same exponential function $e^x$? 
Is there any way of solving such an equation, or such a problem? Or am I just talking nonsense? I would love to be enlightened by all of you.
Thanks in advance. :)
 A: My approach would be rather simple.
I define the logarithm as
$$\log x =\lim\limits_{h \to 0}\frac{x^h-1}{h}$$
I define $e$ as the unique number such that
$$\log e =1$$
Then, by the property that $$\alpha \log x =\log x^{\alpha}$$

$$\log x^{\alpha} =\lim\limits_{h \to 0}\frac{x^{\alpha h}-1}{h}$$
$$\log x^{\alpha} =\alpha\lim\limits_{h \to 0}\frac{x^{\alpha h}-1}{\alpha h}$$
Now let $\alpha h =t$, from where
$$\log x^{\alpha} =\alpha\lim\limits_{t \to 0}\frac{x^{t}-1}{t}=\alpha \log x$$

it is clear that multiplying by $x$
$$x \log e =x$$
$$ \log e^x =x$$
so that $e^x$ is the unique number that satisfies
$$ \log e^x =x$$
Then it follows  $y=e^x$ is the the inverse mapping of $y=\log x$.
A: Supposing we have $\ln x$ and not $e^x$, we may as well assume that we've defined $\ln x$ as an anti-derivative of $x^{-1}$, that is:
$$ \ln x = \int_1^x t^{-1} \; dt.$$
This is in fact a standard approach that can be taken to define logarithms and exponentials in Calc I or II (see Stewart's "Gray Pages" in Calculus and elsewhere).
Then we get $(\ln x)' = x^{-1}$.  If $g(x)$ is an inverse for $f(x) = \ln x$, then
$$ g'(x) = \frac{1}{f'(g(x))} = \frac{1}{(g(x))^{-1}} = g(x).$$
In other words, the inverse function of $\ln x$ satisfies the differential equation $g'(x) = g(x)$.  Furthermore, we have $g(0) = 1$ (since $\ln 1 = 0$).  At this point, if we've defined $e^x$ in some other context, then we find that $g(x)=e^x$ does satisfy the initial value problem.  By uniqueness, $g(x) = e^x$ must be the inverse of $\ln x$.
Hope this helps!
A: Sorry, but your first approach looks a bit strange. The map $y \mapsto \log y$ (suitably defined) can be inverted. But how can you say that its inverse has the form $x \mapsto A^x$ for some $A>0$? If you know this, then it follows easily that $A=e$. To understand the subtle inconsistency of your question, reverse it: assume that $x \mapsto e^x$ is invertible. Is it meaningful to ask for what value of $b \neq 1$ the inverse has the form $y \mapsto \log_b y$? I guess not.
A: I don't know the level at which to answer this question but here goes: It depends on how you are 'defining the functions in question' and then, once defined you either prove the other definitions are equivalent - or just prove the inverse is exp(x). For instance, let's define (for x > 0)  ln x = integral 1 to x of dt/t... from this definition it becomes clear that ln so defined is A logarithm function. Then the natural definition for e is the x for which ln x = 1. But now you want to prove either that this is the same e as one defined in another way, or you want to prove that e^x is the inverse function of ln x (this follows the way we have defined e and ln here by 5Tom's and Gedgar's comments) So maybe you want to show that with this definition of e, d/dx (e^x) = e^x, but this follows as ln is differentiable with everywhere positive derivative on it's domain, so d/dx(e^(ln x)) on the one hand is 1 on the other hand is (1/x)(d/dx e^u)|u=ln x, which gives you the result you want. If there are other identities you want to show are this same e, this can be the building block.
