How to derive that for every real $y > 0$, for every positive real $z \neq 1$, there is a $x \in \mathbb{R}$ such that $y=z^x$. I am not sure on how to derive the following statement concerning the reals (that I think should be true).

For every real $y > 0$, for every positive real $z \neq 1$, there is a $x \in \mathbb{R}$ such that $y=z^x$.

QUESTIONS:


*

*Is this part of the definition of exponentiation, or it is a result that can be proven?

*If it can be proven, how (maybe by using the Archimedean Property)?
Thank you for your time.
PS: Few days ago I asked almost the same question, but a user pointed out (rightly) that the question I really wanted to ask is the one here.
 A: Since the exponential function $\exp(t) = e^t$ strictly increases on $\mathbb{R}$, (Check this in your analysis textbook) its inverse, the logarithmic function $\log t$ on $\mathbb{R}^+$ is well-defined. If we take $x = \log y / \log z$, $ z^x = e^{\log y} = y$ clearly.
A: You can use the fact that $\mathbb{R}$ has the least upper bound property. Let $E$ be the set of all $t$ such that $t^n \lneq x$, then if we can show that $E$ is nonempty and bounded above, we are guaranteed the existence of $y =sup$  $E$  in $\mathbb{R}$. From there, if we assume that $ y^n \lneq x$ or $y^n \gneq x$ we should be able to obtain a contradiction (or else we would have produced a "gap" in the real line). 
The uniqueness part of the proof is much easier since if a number had two distinct real nth roots, then one would necessarily be larger than the other. 
Also this is not a part of the definition of exponentiation. Note that we can take exponents in $\mathbb{Q}$ but the statement you asked about no longer holds. So this is indeed something that must be proven.
A: $$y = a^{\log_a(y)} \to z=a, x=\log_a (y)$$
