Avoiding circularity in explaining the meaning of real exponents In an answer to 'What does $2^x$ really mean when $x$ is not an integer?' Álvaro Lozano-Robledo explains that we can understand real number exponents in terms of the definition of $\log(x)$:
$$\log(x) := \int_1^x \frac{1}{t} dt$$
I understand that one can then define $e^x$ as the inverse function of $\log(x)$. In his answer he then shows that what $a^x$ really means for any real number base $a > 0$ and exponent $x$ can be defined in terms of $\log(x)$ and its inverse $e^x$ in the following way:
$$a^x = e^{\log(a^x)} = e^{x\log(a)}$$
But this definition seems to rely on the logarithm power property $\log(a^x)=x\log(a)$. My question is, how can this property be proven without already knowing what $a^x$ means for real numbers $a > 0$ and $x$?
My attempt at answering the question before posting it here yielded the following:
ProofWiki has a proof of the logarithm power property that depends on a proof of the power rule for derivatives with real number index. However, this last proof also seems to assume that the meaning of $a^x$ for real numbers $a > 0$ and $x$ is known. 
P.S. I have not yet had the time to study calculus/analysis formally. Which means that this might all become obvious after reading some rigorous analysis book. 
 A: Just take $$a^x := \exp(x \log a)$$ as the definition. Then, taking log on both sides, the property $$\log(a^x) = x \log a$$ follows as a logical consequence. 
A: There are many approaches to define $a^{x}$ when $x$ is irrational. Note that if we are restricted to real numbers then we must have $a > 0$ for $a^{x}$ to make sense. The simplest (but non-intuitive) approach is to first develop a theory of logarithmic and exponential functions namely $\log x$ and $\exp(x)$. Since these are inverses to each other we only need to define one of them and treat the other as inverse. Once these functions are available we define $$a^{x} = \exp(x\log a)\tag{1}$$ This is a definition and it does not rely on any other result. However it is easy to see the motivation behind this definition.
Suppose initially that $x$ is a positive integer then $$\log(a^{x}) = \log(a\cdot a\cdots a\text{ upto }x\text{ times}) = \log a + \log a + \cdots + \log a\text{ upto }x\text{ times} = x\log a$$ If $x$ is a positive rational number say $p/q$ then $\{a^{x}\}^{q} = a^{p}$ and from what we have proved above this leads to $$q\log a^{x} = p\log a$$ so that $$\log a^{x} = (p/q)\log a = x\log a$$ Next let $x$ be a negative rational number so that $x = -y$ where $y \in \mathbb{Q}^{+}$. Then $$\log a^{x} = \log 1/a^{y} = -\log a^{y} = -y\log a = x\log a$$ Further note that $\log a^{x} = x\log a$ holds trivially when $x = 0$. It proves that the identity $$\log a^{x} = x\log a$$ is true for all rationals $x$ and we want this identity to hold for irrational values of $x$ also. Therefore it is essential to define $a^{x}$ as $\exp(x\log a)$. Thus the motivation for the definition $a^{x} = \exp(x\log a)$ is to extend the identity $\log a^{x} = x\log a$ for irrational values of $x$ also.

Another approach (which is more intuitive) to define $a^{x}$ is by taking a sequence $x_{n}$ of rationals tending $x$ and then define $$a^{x} = \lim_{n \to \infty}a^{x_{n}}\tag{2}$$ When we use this approach the definition of $\log$ comes later via the limit $$\log a = \lim_{x \to 0}\frac{a^{x} - 1}{x}\tag{3}$$ and $\exp$ is defined by $\exp(x) = y$ if $x = \log y$. Under this approach the equation $$a^{x} = \exp(x\log a)$$ becomes a result based on the definitions of $a^{x}, \log, \exp$.
A: By witing 
$$
a^{\,x} \quad \left| \begin{gathered}
  \;0 < \;a \in \;\;\mathbb{R}\,\, \hfill \\
  \;x \in \;\;\mathbb{R}\,\, \hfill \\ 
\end{gathered}  \right.$
$$
it is assumed that you want to keep some
"resemblance" with the function $a^n$.
Suppose you want to keep the property of addition of the exponents
$$
a^{\,x + y}  = a^{\,x} a^{\,y} 
$$
so that:
$$
\begin{gathered}
  a^{\,x} a^{\,n - x}  = a^{\,n}  \hfill \\
  \left( {a^{\,x} } \right)^{\,n}  = a^{\,n\,x}  \hfill \\
  \frac{1}
{{a^{\,x} }} = \left( {\frac{1}
{a}} \right)^{\,x}  = a^{\, - \,\,x}  \hfill \\
  \left( {a^{\,x} } \right)^{\,m/n}  = \left( {a^{\,m/n} } \right)^{\,x}  = a^{\,x\,m/n}  \hfill \\ 
\end{gathered} 
$$
then by putting x as the limit of a rational sequence
$$
x = \mathop {\lim }\limits_{n\, \to \,\infty } \left\{ {r_1 , \cdots ,r_n , \cdots } \right\}
$$
$a^x$ can be defined as:
$$
a^{\,x}  = \mathop {\lim }\limits_{n\, \to \,\infty } \left\{ {a^{\,r_{\,1} } , \cdots ,a^{\,r_{\,n} } , \cdots } \right\}
$$
and it follows that
$$
\left( {a^{\,x} } \right)^{\,y}  = \left( {a^{\,y} } \right)^{\,x}  = a^{\,x\,y} 
$$
$$
a^{\,x}  = \left( {e^{\,\ln a} } \right)^x  = e^{\,x\,\ln a} 
$$
