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.