|Description: Define the number 2.
Note that the numbers 0 and 1 are constants defined as primitives of the
complex number axiom system (see df-0 6759 and df-1 6760).
Note: Only the digits 0 through 9 (df-0 6759
through df-9 7494) and the
number 10 (df-10 7495) are explicitly defined. Integers can be
as sums of powers of 10 or as some other expression built from operations
on the numbers 0 through 10. For example, the prime number 823541 can be
expressed as . Decimals can be expressed as ratios of
integers, as in cos2bnd 9139. (Fortunately, 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.)
A decimal representation of numbers may be added at some point in the
future if it is deemed useful. Ideas for a clean, eliminable definition
are welcome. (An awkward earlier definition was deleted from the database