Natural number exponentiation


Definition

  power_0: ?a ^ 0 = 1
power_Suc: ?a ^ Suc ?n = ?a * ?a ^ ?n
THEOREM   

One is a right identity element of natural number exponentiation.

$$\forall x \in \mathbb{N} : x^1 = x$$

Proof unavailable

THEOREM   

Exponentiation is right-distributive over multiplication.

$$\forall x,y,z \in \mathbb{N} : (xy)^z = x^zy^z$$

Proof available

THEOREM    \(\forall x,y,z \in \mathbb{N} : x^{y + z} = x^yx^z\)

Proof available

THEOREM    \(\forall x,y,z \in \mathbb{N} : x^{yz} = \left(x^y\right)^z\)

Proof available