Proof of Powers of Natural Numbers with Zero

Throughout, $0+1=1$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (i); for $k\in\mathbb{N}_{0}$, $k+1$ is the successor of $k$ and hence a natural number, by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (v) and Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (i); and $k<k+1$ for $k\in\mathbb{N}$, by Arithmetic and Order of the Natural Numbers (xi).

The multiplication of $\mathbb{N}_{0}$ has the neutral element $1=S(0)$, by Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order (iii) and The Set of Natural Numbers and the Number One (ii), so the powers are defined for every exponent in $\mathbb{N}_{0}$.

Closure. By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (iii), applied to the multiplication of $\mathbb{N}_{0}$ and $x=m$, there is a map $p:\mathbb{N}_{0}\to\mathbb{N}_{0}$ with $p(k)=m^{k}$ for every $k$; hence $m^{k}\in\mathbb{N}_{0}$.

Recursion. $m^{0}=1$ by Powers with Exponents in the Natural Numbers with Zero (ii), $1$ being the neutral element. For $k=0$, the power $m^{1}=\prod_{i=1}^{1}m$ is the value at $1$ of the map of Iterating a Binary Operation along a Finite List (i), which is $m$, so

$$m^{0+1}=m=1\cdot m=m^{0}\cdot m$$

by Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order (iii). Let now $k\ge1$, put $n=k+1\in\mathbb{N}$, and let $s:[n]\to\mathbb{N}_{0}$ be the map of Iterating a Binary Operation along a Finite List (i) for the multiplication of $\mathbb{N}_{0}$ and the map $[n]\to\mathbb{N}_{0}$ whose value at every $i\in[n]$ is $m$ (Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (i)), so that $m^{n}=s(n)$ by Iterated Operations: Finite Sums and Finite Products (i). As $k\in[n]$ and $k<n$,

$$m^{k+1}=s(k+1)=s(k)\cdot m.$$

The restriction of $s$ to $[k]$ satisfies $s(1)=m$ and $s(i+1)=s(i)\cdot m$ for $i\in[k]$ with $i<k$, so by the uniqueness in Iterating a Binary Operation along a Finite List (i) it is the map for $[k]$ and the map with value $m$ at every $i\in[k]$, whence $s(k)=\prod_{i=1}^{k}m=m^{k}$ by Iterated Operations: Finite Sums and Finite Products (i) and Powers with Exponents in the Natural Numbers with Zero (i). Thus $m^{k+1}=m^{k}\cdot m$.

For the remaining clauses we read natural numbers in $\mathbb{R}$, writing $u_{\mathbb{R}}$ for the image of $u\in\mathbb{N}_{0}$; $\mathbb{R}$ is a commutative ring and an ordered field. For $u,v,i\in\mathbb{N}_{0}$, the images of products and powers are formed in $\mathbb{R}$,

$$(uv)_{\mathbb{R}}=u_{\mathbb{R}}\,v_{\mathbb{R}},\qquad(u^{i})_{\mathbb{R}}=(u_{\mathbb{R}})^{i},$$

by The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (iii) and The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (v), and $0_{\mathbb{R}}$ and $1_{\mathbb{R}}$ are the zero and the unit of $\mathbb{R}$ by The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (i). Powers in $\mathbb{R}$ obey Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality. Two elements of $\mathbb{N}_{0}$ with equal images are equal, by Reading Natural Numbers in ℝ: Injectivity, Order and Pascal's Rule (i); so each identity below follows from the identity of the images of its two sides.

Sum of exponents. By Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (i),

$$(m^{j+k})_{\mathbb{R}}=(m_{\mathbb{R}})^{j+k}=(m_{\mathbb{R}})^{j}\,(m_{\mathbb{R}})^{k}=(m^{j}\,m^{k})_{\mathbb{R}}.$$

Product of bases. By Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (ii),

$$\big((mn)^{k}\big)_{\mathbb{R}}=(m_{\mathbb{R}}\,n_{\mathbb{R}})^{k}=(m_{\mathbb{R}})^{k}\,(n_{\mathbb{R}})^{k}=(m^{k}\,n^{k})_{\mathbb{R}}.$$

Bases one and zero. By The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (v) and The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (i), $(1^{k})_{\mathbb{R}}=(1_{\mathbb{R}})^{k}$ with $1_{\mathbb{R}}$ the unit of $\mathbb{R}$, and $(1_{\mathbb{R}})^{k}=1_{\mathbb{R}}$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (ii); so $1^{k}=1$. Next, $0^{k+1}=0^{k}\cdot0=0$ by (ii) and Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order (i).

Positivity. Let $1\le m$. By Reading Natural Numbers in ℝ: Injectivity, Order and Pascal's Rule (ii), $1_{\mathbb{R}}\le m_{\mathbb{R}}$, so $1_{\mathbb{R}}\le(m_{\mathbb{R}})^{k}=(m^{k})_{\mathbb{R}}$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (x), and Reading Natural Numbers in ℝ: Injectivity, Order and Pascal's Rule (ii) again gives $1\le m^{k}$.