# Finite Ordinal Times Ordinal

## Theorem

Let $m$ and $n$ be finite ordinals.

Let $m \ne 0$, where $0$ is the zero ordinal.

Let $x$ be a limit ordinal.

Then:

$m \times \paren {x + n} = x + \paren {m \times n}$

## Proof

### Lemma

Let $m$ be a finite ordinal.

Let $m \ne 0$, where $0$ is the zero ordinal.

Then:

$m \times \omega = \omega$

where $\omega$ denotes the minimally inductive set.

$\Box$

$m \times \paren {x + n} = \paren {m \times x} + \paren {m \times n}$

It remains to prove that $x = m \times x$.

Since $x$ is a limit ordinal, it follows that:

 $\ds \exists y \in \On: \,$ $\ds x$ $=$ $\ds \omega \times y$ Factorization of Limit Ordinals $\ds m \times x$ $=$ $\ds m \times \paren {\omega \times y}$ Substitutivity of Class Equality $\ds m \times x$ $=$ $\ds \paren {m \times \omega} \times y$ Ordinal Multiplication is Associative $\ds$ $=$ $\ds \omega \times y$ lemma

$\blacksquare$