$x^n y^n = (xy)^n$, proof exercise

Question

As an exercise, I tried to prove the following theorem. Please share your thoughts about what I wrote. (The proof only uses the utensils which are listed below.)

---

Theorem

\begin{equation*} x^n y^n = (xy)^n \qquad \qquad \forall n \in \mathbb{N}, \; x,y \in \mathbb{R} \end{equation*}

---

Proof

First, introducing a predicate $P$ over $\mathbb{N}$, we rephrase the theorem as follows. \begin{equation*} \forall n \in \mathbb{N} : P(n), \end{equation*} where \begin{equation*} P(n) \quad := \quad \forall x, y \in \mathbb{R} : x^n y^n = (xy)^n. \end{equation*}

We prove the theorem by induction on $n$.

$\textbf{Basis: }$ $P(0)$

Let $x, y \in \mathbb{R}$. \begin{equation*} \begin{split} x^0 y^0 & = (x^0) (y^0) && \\ & = (1 ) (1 ) && | \text{ zero-th power definition (see utensils below)} \\ & = 1 \cdot 1 && \\ & = 1 && | \text{ multiplicative identity} \\ & = (xy)^0 && | \text{ closure u. m. & zero-th power d.} \\ \end{split} \end{equation*}

$\textbf{Inductive step: }$ $\forall n \in \mathbb{N} : \big( P(n) \Rightarrow P(n + 1) \big)$

Let $n \in \mathbb{N}$. We assume $P(n)$. Let $x, y \in \mathbb{R}$. \begin{equation*} \begin{split} x^{(n + 1)} y^{(n + 1)} & = \big( x^{(n + 1)} \big) \big( y^{(n + 1)} \big) && \\ & = ( x^{n} x ) ( y^{n} y ) && | \text{ nonzero-th power d.} \\ & = x^{n} x y^{n} y && | \text{ generalised a. l.} \\ & = x^{n} y^{n} x y && | \text{ generalised c. l.} \\ & = ( x^{n} y^{n} ) x y && | \text{ generalised a. l.} \\ & = \big( (xy)^n \big) x y && | \text{ } P(n) \\ & = (xy)^n (x y) && | \text{ generalised a. l.} \\ & = (xy)^{(n + 1)} && | \text{ closure u. m. & nonzero-th power d.} \\ \end{split} \end{equation*}

QED

---

Utensils

$\textbf{zero-th power definition: }$ $ \forall x \in \mathbb{R} : x^0 := 1 $

$\textbf{nonzero-th power definition: }$ $ \forall n \in \mathbb{N}, x \in \mathbb{R} : x^{(n + 1)} := x^{n} x $

$\textbf{closure under multiplication: }$ $ \forall x,y \in \mathbb{R} : xy \in \mathbb{R} $

$\textbf{multiplicative identity: }$ $ \forall x \in \mathbb{R} : 1x = x $

$\textbf{generalised associative law: }$ concerning $\mathbb{R}$, see Wikipedia

$\textbf{generalised commutative law: }$ concerning $\mathbb{R}$, $\dots$

Answer 1

If the question is "Is this correct?", the answer is yes. :-)