Finite Ordinal Times Ordinal

From ProofWiki
Jump to navigation Jump to search


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

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

Let $x$ be a limit ordinal.


$m \times \left({ x + n }\right) = x + \left({ m \times n }\right)$


By Ordinal Multiplication is Left Distributive, it follows that:

$m \times \left({ x + n }\right) = \left({ m \times x }\right) + \left({ m \times n }\right)$

It remains to prove that $x = \left({ m \times x }\right)$.

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

\(\, \displaystyle \exists y \in \operatorname{On}: \, \) \(\displaystyle x\) \(=\) \(\displaystyle \left({\omega \times y}\right)\) Factorization of Limit Ordinals
\(\displaystyle m \times x\) \(=\) \(\displaystyle m \times \left({\omega \times y}\right)\) Substitutivity of Class Equality
\(\displaystyle m \times x\) \(=\) \(\displaystyle \left({m \times \omega}\right) \times y\) Ordinal Multiplication is Associative
\(\displaystyle \) \(=\) \(\displaystyle \omega \times y\) by lemma