# Upper Bound of Ordinal Sum

## Theorem

Let $x$ and $y$ be ordinals.

Suppose $x > 1$.

Let $\sequence {a_n}$ be a finite sequence of ordinals such that:

$a_n < x$ for all $n$

Let $\sequence {b_n}$ be a strictly decreasing finite sequence of ordinals such that:

$b_n < y$ for all $n$

Then:

$\ds \sum_{i \mathop = 1}^n x^{b_i} a_i < x^y$

## Proof

The proof shall proceed by finite induction on $n$:

For all $n \in \N_{\ge 0}$, let $\map P n$ be the proposition:

$\ds \sum_{i \mathop = 1}^n x^{b_i} a_i < x^y$

### Basis for the Induction

$\map P 0$ says that:
$\ds \sum_{i \mathop = 1}^0 x^{b_i} a_i < x^y$
 $\ds \sum_{i \mathop = 1}^0 x^{b_i} a_i$ $=$ $\ds 0$ Definition of Ordinal Sum $\ds$ $<$ $\ds x^y$ Exponent Not Equal to Zero

This is our basis for the induction.

$\Box$

### Induction Hypothesis

Now we need to show that, if $\map P k$ is true, where $k \ge 0$, then it logically follows that $\map P {k + 1}$ is true.

So this is our induction hypothesis:

$\ds \sum_{i \mathop = 1}^k x^{b_i} a_i < x^y$

Then we need to show:

$\ds \sum_{i \mathop = 1}^{k \mathop + 1} x^{b_i} a_i < x^y$

### Induction Step

This is our induction step:

By the inductive hypothesis:

$\ds \sum_{i \mathop = 1}^k x^{b_{i + 1}} a_{i + 1} < x^{b_1}$ since $b_1$ is greater than all $b_i$ for $i > 1$.

Then:

 $\ds \sum_{i \mathop = 1}^{k + 1} x^{b_i} a_i$ $=$ $\ds x^{b_1} a_1 + \sum_{i \mathop = 1}^k x^{b_{i + 1} } a_{i + 1}$ General Associative Law for Ordinal Sum $\ds$ $<$ $\ds x^{b_1} a_1 + x^{b_1}$ Membership is Left Compatible with Ordinal Addition $\ds$ $=$ $\ds x^{b_1} a_1^+$ Ordinal Multiplication is Left Distributive $\ds$ $\le$ $\ds x^{b_1^+}$ Membership is Left Compatible with Ordinal Multiplication and Successor of Element of Ordinal is Subset $\ds$ $\le$ $\ds x^y$ Membership is Left Compatible with Ordinal Exponentiation and Successor of Element of Ordinal is Subset

So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.

Therefore:

$\ds \sum_{i \mathop = 1}^n a_i x^{b_i} < x^y$

$\blacksquare$