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. 

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