Rational powers $a^r$ of a positive base

Let $a\in \mathbb{R}$ with $a>0$ and let $r\in \mathbb{Q}$ (The rationals as equivalence classes of pairs of integers).

Every rational has a representative with positive denominator (Every rational has a positive-denominator representative), so write $r=m\mathrm{/}n$ with $m\in \mathbb{Z}$ and $n$ a positive integer; a positive integer is the image of a unique natural $\ge 1$ (The naturals embed in the integers), and we write $n$ for that natural too. Define

$a^r:=(a^{1\mathrm{/}n}{)}^m,$

where $a^{1\mathrm{/}n}$ is the unique nonnegative $n$-th root of $a$ (Existence and uniqueness of $n$-th roots: a unique $a^{1\mathrm{/}n}\ge 0$ with $(a^{1\mathrm{/}n}{)}^n=a$) and the outer exponent is an integer power (Integer powers $a^m$). The outer power is legitimate because $a^{1\mathrm{/}n}>0$ when $a>0$, so it has an inverse and negative integer exponents are allowed.

Well-definedness. The right-hand side must not depend on which representative $m\mathrm{/}n$ of $r$ was chosen. It does not: that is Rational powers do not depend on the representative ↗, which is recorded in this item's justified_by rather than in its deps, since it is a statement about the operation defined here and therefore depends on this definition.

The base must be positive. For $a<0$ the same formula is not a definition at all, because different representatives of the same rational give different answers, or no answer: see FALSE: $a^{m\mathrm{/}n}:=(a^{1\mathrm{/}n}{)}^m$ extends to negative bases, which is exactly the item that justifies the restriction.

Supplementary clause for the base $0$. For $a=0$ and rational $r>0$ (Order on the rationals) the displayed formula still makes sense and still does not depend on the representative: $r>0$ forces $m\ge 1$, and $(0^{1\mathrm{/}n}{)}^m=0^m=0$ (Existence and uniqueness of $n$-th roots: a unique $a^{1\mathrm{/}n}\ge 0$ with $(a^{1\mathrm{/}n}{)}^n=a$ applies to every $a\ge 0$). So we set $0^r=0$ for rational $r>0$. For $r<0$ the expression $0^r$ is left undefined, since $0$ has no inverse. This clause is what lets the inequalities later on this page be stated for nonnegative entries rather than for positive ones only.

• Consistency with integer powers. If $r\in \mathbb{Z}$ then $r=r\mathrm{/}1$, $a^{1\mathrm{/}1}=a$ (Existence and uniqueness of $n$-th roots: a unique $a^{1\mathrm{/}n}\ge 0$ with $(a^{1\mathrm{/}n}{)}^n=a$), and the definition returns $(a^1{)}^r=a^r$ as given by Integer powers $a^m$. So the notation $a^r$ is unambiguous, and rational powers extend integer powers on positive bases. At $r=1\mathrm{/}n$ it returns $(a^{1\mathrm{/}n}{)}^1=a^{1\mathrm{/}n}$, so the root notation of Existence and uniqueness of $n$-th roots: a unique $a^{1\mathrm{/}n}\ge 0$ with $(a^{1\mathrm{/}n}{)}^n=a$ is the special case $r=1\mathrm{/}n$, as intended.
• $a^r>0$ for every $a>0$ and every $r\in \mathbb{Q}$, the exponent $0$ included. Writing $r=m\mathrm{/}n$ with $n\ge 1$: the root $a^{1\mathrm{/}n}$ is positive (Existence and uniqueness of $n$-th roots: a unique $a^{1\mathrm{/}n}\ge 0$ with $(a^{1\mathrm{/}n}{)}^n=a$); for $m\ge 0$ the value $(a^{1\mathrm{/}n}{)}^m$ is a natural power of a positive element, hence positive, which is claim 1 of Monotonicity of $x\mapsto x^n$ and of $n\mapsto a^n$ and covers $m=0$ as well, since $a^0=1>0$; and for $m<0$ the value is $(a^{1\mathrm{/}n}{)}^m=((a^{1\mathrm{/}n}{)}^{-m}{)}^{-1}$ (Laws of integer exponents, claim 2), the inverse of a positive element, hence positive (Inverses of positives are positive, and reciprocation reverses order). Note that Monotonicity of $x\mapsto x^n$ and of $n\mapsto a^n$ is stated for natural exponents only, so it does not by itself settle the negative case; that is what the inverse step is for. The exponent laws are Laws of rational exponents and the order behaviour is Monotonicity of $r\mapsto a^r$ and of $a\mapsto a^r$.
• The exponent is a rational, never a real. Nothing on this page is a limit, a series or a continuous function, and $a^r$ is computed in finitely many field operations once the root is available. What would be needed to go further, why it is deferred here, and where the library later defines $a^x$ for real $x$ are recorded in Why real exponents are deferred on the rational-powers page.
• The convention $0^0=1$ of Integer powers $a^m$ is untouched: $r=0$ is not covered by the supplementary clause, which asks for $r>0$. So $0^0=1$ while $0^r=0$ for every rational $r>0$. There is no inconsistency, only the familiar fact that the two-variable function $(a,r)\mapsto a^r$ has no continuous extension to $(0,0)$, a statement this library cannot even make yet.