Definition:Power (Algebra)/Real Number/Definition 1

Definition

Let $x \in \R_{>0}$ be a (strictly) positive real number.

Let $r \in \R$ be a real number.

We define $x^r$ as:

$x^r := \map \exp {r \ln x}$

where $\exp$ denotes the exponential function.

This definition is an extension of the definition for rational $r$.

This follows from Logarithms of Powers and Exponential of Natural Logarithm: it can be seen that:

$\forall r \in \Q: \map \exp {r \ln x} = \map \exp {\map \ln {x^r} } = x^r$

Work In Progress
In particular: The above assertion is Definition:Power (Algebra)/Real Number/Definition 2: write Exponentiation to Real Number is Extension of Exponentiation to Rational Number to prove it, and invoke it as part of the equivalence definition
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{WIP}} from the code.