How do we know that $\exp(x)$ agrees with raising a number to a rational power? This is motivated by an earlier question of mine, in which I realized I was never really presented a definition of $e^x$, or more generally, what it means to raise a (positive) real number to an irrational power.
I know that the definition of $a^b$ with $a \in \mathbb{R}^+, b \in \mathbb{Q}$ is pretty straightforward in terms of repeated multiplication and the property that $a^{bc}=(a^b)^c$. I also know that one can define $a^b$ where $b \in \mathbb{R} - \mathbb{Q}$ using limits. This is stated, for example, in this Math.SE question.
Other way to define exponentiation with real powers is with the function $\exp(x)$ or $e^x$, which has many equivalent definitions. For example, one may define it as $e^x = \lim\limits_{n \to \infty} (1+\frac{x}{n})^n$, or as the unique solution to $y' = y$ with $y(0)=1$. Wikipedia has a whole page stating these definitions and showing that they are equivalent to each other.
What I haven't seen is a proof that this new $e^x$ behaves just like the old way of doing exponentiation when $x \in \mathbb{Q}$. If I were to guess, I'd say it's related to Wikipedia's fifth defintion: it is the unique (with some conditions) function that satisfies $f(1) = e$ and $f(x+y)=f(x)f(y)$. However, that defintion seems to involve more advanced concepts than the other ones, concepts which I don't really understand right now.
Is there a proof of the fact that $\exp(x)$ is equivalent to the definition of exponentiation for rational powers?
 A: Let $\exp(x)$ denote the exponential function.   You can define this any way that you like, but we will assume the following facts:
Fact 1. The derivative of $\exp(x)$ is $\exp(x)$, and $\exp(0)=1$.
Fact 2.  Let $f(x)$ be any differentiable function.  If $f(0) = 1$ and $f'(x) = f(x)$ for all $x\in\mathbb{R}$, then $f(x) = \exp(x)$ for all $x\in\mathbb{R}$.
We will also assume the Power Rule for rational exponents.  From this, we can prove the following theorem:
Theorem. Let $e = \exp(1)$.  Then $e^q = \exp(q)$ for any rational number $q$.
Proof: Let $q\in\mathbb{Q}$, and let $f\colon\mathbb{R}\to\mathbb{R}$ be the function $f(x) = [\exp(x/q)]^q$. Note that $f(0) = 1^q = 1$.  Furthermore, by the Power Rule and the Chain Rule, we have
$$
f'(x) \;=\; q[\exp(x/q)]^{q-1} \exp(x/q)\, (1/q) \;=\; [\exp(x/q)]^q \;=\; f(x)
$$
It follows that $f(x) =\exp(x)$ for all $x\in\mathbb{R}$, so
$$
\exp(q) \;=\; f(q) \;=\; [\exp(q/q)]^q \;=\; e^q.\tag*{$\square$}
$$
A: Let's use the definition $$e^x=\lim_{n\to\infty}\left(1+{x\over n}\right)^n$$ and prove $e^{pq}=(e^p)^q$. 
We have $$e^{pq}=\lim_{n\to\infty}\left(1+{pq\over n}\right)^n$$ and $$(e^p)^q=\left(\lim_{n\to\infty}\left(1+{p\over n}\right)^n\right)^q=\lim_{n\to\infty}\left(1+{p\over n}\right)^{qn}=\lim_{n\to\infty}\left(1+{pq\over qn}\right)^{qn}=\lim_{m\to\infty}\left(1+{pq\over m}\right)^m$$ which is the same thing. 
But we've now proved the property that you used to define rational powers. 
