Proof:Base b representation

From CS2800 wiki
For all [math]a \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] and [math]b \gt 0 [/math], there exists a sequence [math]\href{/cs2800/wiki/index.php/Sequence_notation}{(d_i)} [/math] of digits satisfying [math]a = \href{/cs2800/wiki/index.php/Base}{(d_i)_b} [/math].

Note that this proof contains an algorithm for finding the digits. Note also that The base b representation is unique.

Proof:
We prove the claim by strong induction on [math]a [/math].


In the base case, we WTS must find a base b representation of 0. The natural choice might be to take the single digit [math]d_0 = 0 [/math]. Then [math]d_0 [/math] is a digit (since [math]0 \lt b [/math]), and clearly [math]0 = \sum d_i b^i = 0 \cdot 1 [/math].

However, when using this proof as an algorithm, it is preferable to take the 'empty' sequence as the representation of 0; otherwise all numbers would have a leading 0. Alternatively, one could give a special case in the inductive step for when [math]a [/math] is already a digit.

For the inductive step, assume that every number less than [math]a [/math] has a base b representation. We wish to show that [math]a [/math] has one also.

We can find the digits by dividing by [math]b [/math]: the last digit [math]d_0 [/math] is given by the remainder, and the rest of the digits are those of the quotient.

Formally, let [math]q := \href{/cs2800/wiki/index.php/Quot}{quot}(a,b) [/math] and [math]r := \href{/cs2800/wiki/index.php/Rem}{rem}(a,b) [/math]. Let [math]\href{/cs2800/wiki/index.php/Sequence_notation}{(d_i)'} [/math] be the base b representation of [math]q [/math] (which we know exists by the inductive hypothesis).

Let [math]d_0 := rem(a,b) [/math], and let [math]d_{i+1} := d_i' [/math]. We have

[math]\begin{align} (d_i)_b &= \sum_{i=0}^{k+1} d_i b^i && \href{/cs2800/wiki/index.php/Base_b_representation}{\text{by definition}} \\ &= \sum_{i=1}^{k+1} d_i b^i + d_0b^0 && \href{/cs2800/wiki/index.php?title=Algebra&action=edit&redlink=1}{\text{algebra}} \\ &= \sum_{j=0}^{k} d_{j+1}b^{j+1} + d_0b^0 && \text{by letting j+1 = i} \\ &= b \sum_{j=0}^k d_j'b^j + d_0b^0 && \text{factor out b and use definition of } d_{j+1} \\ &= b (d_j')_b + d_0b^0 = qb + r = a && \href{/cs2800/wiki/index.php/Base_b_interpretation}{\text{by definition}} \\ \end{align} [/math]