A decision problem is AC⁰ definable, that is, definable in FO($\le, +, \times$), if and only if it is bit-definable, that is, definable by a prenex sentence of FO($\le, +$, BIT). One direction defines the map $i \mapsto 2^i$ from addition and multiplication, by guessing a doubling chain. The other defines multiplication from BIT, which rests on the Bit Sum Lemma, counting the ones of a word of logarithmic length; the product is then assembled from its columns with guessed carry chains. This is the identification of the two vocabularies in Immerman's Descriptive Complexity, Theorem 1.17.