Table of Contents - 5.4.3. Decimal representation of numbers

The decimal representation of numbers/integers is based on the decimal digits
0 through 9 (df-0 through df-9), which are explicitly defined in the
following. Note that the numbers 0 and 1 are constants defined as primitives
of the complex number axiom system (see df-0 and df-1).

With the decimal constructor df-dec, it is possible to easily express
larger integers in base 10. See deccl and the theorems that follow it.
See also 4001prm (4001 is prime) and the proof of bpos. Note that
the decimal constructor builds on the definitions in this section.

Note: The number 10 will be represented by its digits using the decimal
constructor only, i.e., by . Therefore, only decimal digits are
needed (as symbols) for the decimal representation of a number.

Integers can also be exhibited as sums of powers of 10 (e.g. the number 103
can be expressed as ) or as some other expression
built from operations on the numbers 0 through 9. For example, the prime
number 823541 can be expressed as . Decimals can be
expressed as ratios of integers, as in cos2bnd.

Most abstract math rarely requires numbers larger than 4. Even in Wiles'
proof of Fermat's Last Theorem, the largest number used appears to be 12.