Prove $e^{\ln{x}} = x$
Is it possible to prove $e^{\ln{x}} = x$ for a student or can you only say that exponentiation is defined to be the inverse of natural logarithm and stop there?
For a student. Let $x>0$. Then
\begin{align*} e^{ln x} &= x \\ \Leftrightarrow \ln\left(e^{ln x}\right) &= \ln x \\ \Leftrightarrow \ln x \cdot \ln e &= \ln x \\ \Leftrightarrow \ln x \cdot 1 &= \ln x \\ \Leftrightarrow \ln x &= \ln x \\ \Leftrightarrow x &= x. \end{align*}
$ \therefore e^{ln x} = x \, \forall \, x>0.$
Appealing to the fact that $\log a^b=b \cdot \log a$ is perfectly acceptable, as it is a prerequisite for being in the club of people who are allowed to express logarithms.
As my commenters rightfully state, this identity proof is best shown in both directions, with the caveat that $x>0$.
Usually I define the function $\exp(x)$ by being the only continuous function such that $\exp(0)=1$ and $\exp'(x)=\exp(x)$ (it is equal to its derivative).
I define $\log(x)=\int_1^x\frac{dx}{x}$.
Then, I define $f(x)=\exp(\ln(x))$.
By definition, f(1)=1, and $f$ is defined on $(0,\infty)$.
Then I apply the usual definition of derivative.
$f'(x)=\frac{f(x)}{x}$. So $f'(1)=1$.
$f''(x)=\frac{xf'(x)-f(x)}{x^2}=0$.
So $f(1)=f'(1)=1$ and $f''(x)=0$. You deduce that $f(x)=x$.
There's a variety of good ways to define the exponential function, and infinitely many bad ways. Here's a (necessarily incomplete) list of good ones.
By power series (but you have to prove the series converges). $$\exp : \mathbb{R} \rightarrow \mathbb{R}^+, \;\;\exp(x) = \sum_{n=0}^\infty \frac{x^n}{n!}$$
As a solution to an initial value problem (but you have to prove a solution exists). $$\exp : \mathbb{R} \rightarrow \mathbb{R}^+, \;\;\exp(0) = 1,\;\; \exp'(x)=\exp(x)$$
Via a well-known limit (but you have to prove convergence). $$\exp : \mathbb{R} \rightarrow \mathbb{R}^+, \;\; \exp(x) = \mathrm{lim}_{n \rightarrow \infty} \left(1+\frac{x}{n}\right)^n$$
As a function that is undone by the logarithm (but you have to prove that there exists a unique function with this property, or in other words that the logarithm is invertible). $$\exp : \mathbb{R} \rightarrow \mathbb{R}^+,\;\;\log(\exp(x)) = x$$
Note that in each case, we're implicitly asserting that the equation of interest holds for all $x$ in the domain of $\exp$, namely $\mathbb{R}.$
Personally, I like definition 4 best, because the others are "too clever." Math is best when there's no "magic," and the reader ends up feeling like they could have worked it all out themselves, had they just the time and the motivation. So, we must define the (natural) logarithm first. As with the exponential function, there's a variety of good ways of doing this, and infinitely many bad ways. Here's the only good way that I know of.
$$\log : \mathbb{R}^+ \rightarrow \mathbb{R},\;\;\log(x) = \int_1^x\frac{dy}{y}$$
Now, it is necessary to prove that this integral exists. However, if $1/y$ is known to be continuous on $\mathbb{R}^+,$ then existence is immediate.
Furthermore, it is necessary to prove invertibility. However, since $1/y$ is strictly positive on $\mathbb{R}^+$, thus $\log$ is a strictly increasing function. Therefore, $\log$ is injective (or 'one-to-one'). So all that remains to show is that $\log$ is surjective (or 'onto'). Once we have surjectivity, it is immediate that $\log$ has an inverse, which we call $\exp$.
So, if we do things this way, it is not necessary to prove that $\exp(\log x) = x$, because it is our very definition.