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. 

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} 
$$
