General Associative Law for Ordinal Sum/Proof 1
Jump to navigation
Jump to search
Theorem
Let $x$ be a finite ordinal.
Let $\sequence {a_i}$ be a sequence of ordinals.
Then:
- $\ds \sum_{i \mathop = 1}^{x + 1} a_i = a_1 + \sum_{i \mathop = 1}^x a_{i + 1}$
Proof
The proof shall proceed by induction on $x$.
Basis for the Induction
If $x = 0$, then:
\(\ds \sum_{i \mathop = 1}^{0 + 1} a_i\) | \(=\) | \(\ds \sum_{i \mathop = 1}^0 a_i + a_1\) | Definition of Ordinal Sum | |||||||||||
\(\ds \) | \(=\) | \(\ds a_1\) | Ordinal Addition by Zero | |||||||||||
\(\ds \) | \(=\) | \(\ds a_1 + \sum_{i \mathop = 1}^0 a_i\) | Ordinal Addition by Zero |
This proves the basis for the induction.
$\Box$
Induction Step
Suppose:
- $\ds \sum_{i \mathop = 1}^{x + 1} a_i = a_1 + \sum_{i \mathop = 1}^x a_{i + 1}$
Then:
\(\ds \sum_{i \mathop = 1}^{x + 2} a_i\) | \(=\) | \(\ds \sum_{i \mathop = 1}^{x + 1} a_i + a_{i + 2}\) | Definition of Ordinal Sum | |||||||||||
\(\ds \) | \(=\) | \(\ds \paren {a_1 + \sum_{i \mathop = 1}^x a_{i + 1} } + a_{i + 2}\) | Inductive Hypothesis | |||||||||||
\(\ds \) | \(=\) | \(\ds a_1 + \paren {\sum_{i \mathop = 1}^x a_{i + 1} + a_{i + 2} }\) | Ordinal Addition is Associative | |||||||||||
\(\ds \) | \(=\) | \(\ds a_1 + \sum_{i \mathop = 1}^{x + 1} a_{i + 1}\) | Definition of Ordinal Sum |
This proves the induction step.
$\blacksquare$