Integer powers $a^m$

Let $a \in \mathbb{R}$, where $\mathbb{R}$ is the ambient ordered field (Ordered field, Field).

Natural exponents. By the recursion theorem (The recursion theorem) applied to the set $\mathbb{R}$, the starting element $1$ and the function $f(x) = x \cdot a$, there is a unique function $\mathbb{N} \to \mathbb{R}$, written $n \mapsto a^n$, with

$a^0 = 1, \qquad a^{n+1} = a^n \cdot a \quad (n \in \mathbb{N}).$

Thus $a^1 = a$, $a^2 = a \cdot a$, and so on. Note that this is defined for every $a$, including $a = 0$.

Negative exponents. If $a \ne 0$ and $n \in \mathbb{N}$ with $n \ge 1$, set

$a^{-n} := (a^n)^{-1}.$

Why that is legitimate. The right-hand side presupposes that $a^n$ is invertible, that is, that $a^n \ne 0$. This is a proof obligation and not an observation, and it is discharged by claim 2 of Laws of integer exponents ↗: for $a \ne 0$ in a field, $a^n \ne 0$ for every $n \in \mathbb{N}$, proved there by induction on $n$ from the fact that a field has no zero divisors (A field has no zero divisors: $ab = 0 \Rightarrow a = 0$ or $b = 0$). That lemma is a statement about the operation introduced here, so it depends on this definition and is recorded in this item's justified_by rather than in its deps (SCHEMA §3). Given $a^n \ne 0$, the value $(a^n)^{-1}$ is a single well-determined element, because multiplicative inverses in a field are unique (Identities and inverses in a field are unique).

Integer exponents. Every integer $m$ (The integers as equivalence classes of pairs of naturals) is either $\iota(n)$ or $-\iota(n)$ for a unique natural $n$, where $\iota$ is the embedding $\mathbb{N} \to \mathbb{Z}$ (The naturals embed in the integers, Arithmetic on the integers). This too is a citation and not a slogan: the order on $\mathbb{Z}$ is total (The integers form a totally ordered ring), so $m \ge 0$ or $m < 0$; the image of $\iota$ is exactly the set of nonnegative integers, and each of them is $\iota(n)$ for a unique natural $n$ (The naturals embed in the integers); and if $m < 0$ then $-m > 0$, by compatibility of the order with addition (The integers form a totally ordered ring), so $-m = \iota(n)$ and $m = -\iota(n)$, with $n$ unique because $\iota$ is injective. The two clauses above therefore define $a^m$ for every $m \in \mathbb{Z}$ whenever $a \ne 0$, and for every $m \in \mathbb{N}$ for arbitrary $a$. The clauses are consistent where they overlap: the only overlap is $m = 0$, where $-\iota(0) = \iota(0)$ and $(a^0)^{-1} = 1^{-1} = 1 = a^0$.

• The convention $0^0 = 1$ is adopted here, and it is not a matter of taste but of agreement with the recursion above: $a^0 = 1$ is the starting value for every $a$, exactly as the empty product is $1$ (Finite sums and finite products, by recursion). This is the convention that makes the empty product, the binomial theorem, and polynomial notation $\sum_k c_k x^k$ work at $x = 0$ without an exception. The competing convention "$0^0$ undefined" belongs to contexts where $x^y$ is studied as a function of two real variables and one wants continuity, which is unavailable and irrelevant here: the exponent in $a^m$ is an integer, never a real.
• $0^n = 0$ for every $n \ge 1$, since $0^{n} = 0^{n-1} \cdot 0 = 0$, a product with a zero factor (Multiplication by zero: $0 \cdot a = 0$); and $0^{-n}$ is not defined for $n \ge 1$, since $0$ has no inverse.
• The exponent is an integer and stays an integer. Rational exponents are a separate construction resting on the existence of roots (Existence and uniqueness of $n$-th roots: a unique $a^{1/n} \ge 0$ with $(a^{1/n})^n = a$, Rational powers $a^r$ of a positive base), and real exponents are not available at this point in the reading order; they are introduced later in Real powers for positive bases, with the zero-base positive-exponent convention ↗ (see Why real exponents are deferred on the rational-powers page).
• The laws $a^{m+n} = a^m a^n$, $(a^m)^n = a^{mn}$ and $(ab)^n = a^n b^n$ are proved, not assumed, in Laws of integer exponents ↗; the order behaviour of $a \mapsto a^n$ is Monotonicity of $x \mapsto x^n$ and of $n \mapsto a^n$.