HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-2 7709
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 6969 and df-1 6970).

Note: Only the digits 0 through 9 (df-0 6969 through df-9 7716) and the number 10 (df-10 7717) are explicitly defined. Integers can be exhibited 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 (7^7) - 2. Decimals can be expressed as ratios of integers, as in cos2bnd 9423. (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 on 18-Sep-1999.)

Assertion
Ref Expression
df-2 |- 2 = (1 + 1)

Detailed syntax breakdown of Definition df-2
StepHypRef Expression
1 c2 7700 . 2 class 2
2 c1 6963 . . 3 class 1
3 caddc 6965 . . 3 class +
42, 2, 3co 4926 . 2 class (1 + 1)
51, 4wceq 1457 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re 7718  2pos 7729  1p1e2 7740  2p2e4 7741  2timesi 7742  3p2e5 7746  4p2e6 7748  5p2e7 7751  6p2e8 7755  7p2e9 7758  8p2e10 7760  2nn 7767  1lt2 7776  halfpos 7815  addltmul 7822  nneo 7946  zeo 7948  eluz2b1 8054  fztp 8402  fzprval 8405  fztpval 8406  sqval 8631  fac2 8715  faclbnd4lem1 8726  bcn2 8749  bcp1m1 8750  hashpr 8775  binom11 9249  climcndslem1 9264  climcndslem2 9265  ege2le3 9343  ef4p 9364  efcnlem 9372  cos2tsin 9414  cos2bnd 9423  eirrlem 9436  odd2np1lem 9531  isprm3 9634  2prm 9638  opoe 9687  pockthlem 9751  pockthg 9752  prmunb 9760  4sqlem18 9801  decexp2 9813  prmlem2 9829  83prm 9832  317prm 9835  1259lem2 9840  1259lem3 9841  1259lem4 9842  1259lem5 9843  2503lem1 9845  2503lem2 9846  2503lem3 9847  4001lem1 9849  4001lem2 9850  4001lem3 9851  4001lem4 9852  vc2 11438  ipval2 11611  ip2i 11737  cos2pi 11852  coskpi 11886  bcp1ctr 11942  bclbnd 11943  prmpiub 11946  prmor3 11947  prmorublem 11948  prmorub 11949  bposlem1 11952  bposlem2 11953  bposlem5 11956  1p1e2apr1 11964  hv2times 12109  pjthlem1 12440  ho2times 12869  stm1addi 13294  staddi 13295  stadd3i 13297  addltmulALT 13495  emcllem7 13514  ovolunlem1 13709  ovolicc1lem 13722  vitalilem2 13769  axlowdimlem4 14521  axlowdimlem13 14530  bpoly1 14734  bpolydiflem 14737  intset 16203
Copyright terms: Public domain