Theorem: Zero Padded Basis Representation

Let $b \in \Z: b > 1$.
Let $m \in \Z_{> 0}$.
For every $n \in \Z_{\ge 0}$ such that $n < b^m$, there exists one and only one sequence $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ such that:
{{begin-eqn}}
{{eqn | n = 1
      | l = n
      | r = \sum_{j \mathop = 0}^{m - 1} r_j b^j
}}
{{eqn | n = 2
      | q = \forall j \in \closedint 0 {m - 1}
      | l = r_j
      | o = \in
      | r = \N_b
}}
{{end-eqn}}

Proof:
=== Case 1 ===
Let $n \in \Z_{> 0} : n < b^m$.
From Basis Representation Theorem  there exists a sequence $\sequence {s_j}_{0 \mathop \le j \mathop \le k}$ such that:
:$(a): \quad \ds n = \sum_{j \mathop = 0}^k s_j b^j$
:$(b): \quad \forall j \in \closedint 0 k: s_j \in \N_b$
:$(c): \quad s_k \ne 0$
First it is shown that:
:$k \le m - 1$
{{AimForCont}}:
:$m - 1 < k$
Then:
{{begin-eqn}}
{{eqn | l = m
      | o = \le
      | r = k
      | c =
}}
{{eqn | ll= \leadsto
      | l = b^m
      | o = \le
      | r = b^k
      | c = Power Function on Integer between Zero and One is Strictly Decreasing
}}
{{eqn | o = \le
      | r = s_k b^k
      | c = as $s_k > 0$
}}
{{eqn | o = \le
      | r = \sum_{j \mathop = 0}^k s_j b^j
      | c = as $b \ge 0$ and $\forall j \in \closedint 0 {k - 1} : s_j \ge 0$
}}
{{eqn | r = n
      | c = 
}}
{{end-eqn}}
This contradicts the premise:
:$n < b^m$
It follows that:
:$k \le m - 1$
Let $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ be the sequence defined by:
:<nowiki>$r_j = \begin {cases}
s_j & : \text{if } j \le k\\
0 & : \text{if } k < j \le m - 1
\end {cases}$</nowiki>
Then:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 0}^{m - 1} r_j b^j
      | r = \sum_{j \mathop = 0}^k r_j b^j + \sum_{j \mathop = k + 1}^{m - 1} r_j b^j
}}
{{eqn | r = \sum_{j \mathop = 0}^k s_j b^j + \sum_{j \mathop = k + 1}^{m - 1} 0 \cdot b^j
      | c = {{Defof|Sequence}} $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$
}}
{{eqn | r = \sum_{j \mathop = 0}^k s_j b^j
}}
{{eqn | r = n
}}
{{end-eqn}}
To show that $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ is unique, let $\sequence {r'_j}_{0 \mathop \le j \mathop \le m - 1}$ be a sequence such that:
:$(1): \quad \ds n = \sum_{j \mathop = 0}^{m - 1} r'_j b^j$
:$(2): \quad \forall j \in \closedint 0 {m - 1}: r'_j \in \N_b$
Since $n > 0$, then: 
:$\exists j \in \closedint 0 {m - 1} : r'_j > 0$ 
Let: 
:$k' = \max \set {j : j \in \closedint 0 {m - 1} \text{ and } r'_j > 0}$
Then:
:$(1): \quad \ds n = \sum_{j \mathop = 0}^{k'} r'_j b^j$
:$(2): \quad \ds \forall j \in \closedint 0 {k'}: r'_j \in \N_b$
:$(3): \quad r_{k'} \ne 0$
and
:$(4): \quad \ds \forall j \in \closedint {k + 1} {m - 1}: r'_j = 0$
By definition the sequence $\sequence {r_j}_{0 \mathop \le j \mathop \le k'}$ is a basis representation for $n$.
From Basis Representation Theorem the basis representation for $n$ is unique.
Then:
:$\sequence {r'_j}_{0 \mathop \le j \mathop \le k'} = \sequence {s_j}_{0 \mathop \le j \mathop \le k} = \sequence {r_j}_{0 \mathop \le j \mathop \le k}$
That is:
:$k' = k$
and
:$\forall j \in \closedint 0 k :r'_j = r_j$ 
It follows that:
:$\forall j \in \closedint {k + 1} {m - 1}: r'_j = 0 = r_j$
So: 
:$\forall j \in \closedint 0 {m - 1}: r'_j = r_j$
This establishes that the sequence $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ is unique.
{{qed|lemma}}
=== Case 2 ===
Let $n = 0$.
Let $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ be the sequence defined by:
:$\forall j \in \closedint 0 {m - 1} : r_j = 0$.
Then:
:$\ds \sum_{j \mathop = 0}^{m - 1} r_j b^j = \sum_{j \mathop = 0}^{m - 1} 0 \cdot b^j = 0$
This shows that $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ is a sequence such that:
:$(1): \quad \ds 0 = \sum_{j \mathop = 0}^{m - 1} r_j b^j$
:$(2): \quad \forall j \in \closedint 0 {m - 1}: r_j \in \N_b$
Let $\sequence {r'_j}_{0 \mathop \le j \mathop \le m - 1}$ be a sequence such that:
:$(1): \quad \ds 0 = \sum_{j \mathop = 0}^{m - 1} r'_j b^j$
:$(2): \quad \forall j \in \closedint 0 {m - 1}: r'_j \in \N_b$
Suppose for some $i \in \closedint 0 {m - 1}$, $r'_i > 0$.
Then:
:$\ds \sum_{j \mathop = 0}^{m - 1} r'_j b^j \ge r'_i b^i > 0$.
It follows that:
:$\forall j \in \closedint 0 {m - 1} : r'_j = 0$.
This proves that $0$ has one and only one sequence $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ such that:
:$(1): \quad \ds 0 = \sum_{j \mathop = 0}^{m - 1} r_j b^j$
:$(2): \quad \forall j \in \closedint 0 {m - 1}: r_j \in \N_b$
{{qed}}