Reading an integer in base 2

The definition

Let (c₀, …, c_k) be a family of digits equal to 0 or 1, with c_k ≠ 0. Write

   ‾c_k c_{k−1} … c₁ c₀‾ ²  =  sum of c_i · 2^i , for i from 0 to k

We say that (c₀, …, c_k) is the base-2 expansion of n when n equals this sum.

The idea of the proof

Everything rests on one observation: isolating the term of index 0,

   n = c₀ + 2·(c₁ + c₂·2 + … + c_k·2^{k−1})

The factor in brackets is an integer, and c₀ is 0 or 1. But the expression n = 2q + r with r in {0, 1} is unique: it is the Euclidean division by 2. So c₀ is necessarily the remainder of n modulo 2, and (c₁, …, c_k) is an expansion of the quotient.

Everything else follows

This remark turns a question of existence and uniqueness into a plain strong induction: the quotient is strictly smaller than n, so the induction hypothesis applies to it. The digit c₀ is forced, and so are the others by induction — hence uniqueness, and existence by construction.

It is also the algorithm everyone knows: divide by 2, note the remainder, repeat, then read the remainders backwards.

   41 = 2×20 + 1     remainder 1
   20 = 2×10 + 0     remainder 0
   10 = 2×5  + 0     remainder 0
    5 = 2×2  + 1     remainder 1
    2 = 2×1  + 0     remainder 0
    1 = 2×0  + 1     remainder 1

   so 41 is written 101001 in base 2