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

Definition df-2 7750
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 7006 and df-1 7007).

Note: Only the digits 0 through 9 (df-0 7006 through df-9 7757) and the number 10 (df-10 7758) 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 9439. (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 7741 . 2 class 2
2 c1 7000 . . 3 class 1
3 caddc 7002 . . 3 class +
42, 2, 3co 4935 . 2 class (1 + 1)
51, 4wceq 1457 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re 7759  2pos 7770  1p1e2 7781  2p2e4 7782  2timesi 7783  3p2e5 7787  4p2e6 7789  5p2e7 7792  6p2e8 7796  7p2e9 7799  8p2e10 7801  2nn 7808  1lt2 7817  halfpos 7856  addltmul 7863  nneo 7987  zeo 7989  eluz2b1 8095  fztp 8445  fzprval 8448  fztpval 8449  sqval 8674  fac2 8758  faclbnd4lem1 8769  bcn2 8792  bcp1m1 8793  hashpr 8819  binom11 9295  climcndslem1 9310  climcndslem2 9311  ege2le3 9363  ef4p 9384  efcnlem 9392  cos2tsin 9430  cos2bnd 9439  eirrlem 9453  odd2np1lem 9550  isprm3 9653  2prm 9657  opoe 9706  pockthlem 9770  pockthg 9771  prmunb 9779  prmreclem2 9782  4sqlem19 9828  decexp2 9840  prmlem2 9856  83prm 9859  317prm 9862  1259lem2 9867  1259lem3 9868  1259lem4 9869  1259lem5 9870  2503lem1 9872  2503lem2 9873  2503lem3 9874  4001lem1 9876  4001lem2 9877  4001lem3 9878  4001lem4 9879  vc2 11480  ipval2 11652  ip2i 11778  ovolunlem1 11942  ovolicc1lem 11955  vitalilem2 12006  itgcnlem 12162  cos2pi 12395  coskpi 12431  emcllem7 12521  basellem3 12527  basellem5 12529  basellem8 12532  bcp1ctr 12540  bclbnd 12541  prmpiub 12544  prmor3 12545  prmorublem 12546  prmorub 12547  bposlem1 12550  bposlem2 12551  bposlem6 12555  1p1e2apr1 12563  hv2times 12708  pjthlem1 13039  ho2times 13468  stm1addi 13893  staddi 13894  stadd3i 13896  addltmulALT 14094  axlowdimlem4 14768  axlowdimlem13 14777  bpoly1 14981  bpolydiflem 14984  intset 16449
Copyright terms: Public domain