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

Definition df-2 7745
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 6999 and df-1 7000).

Note: Only the digits 0 through 9 (df-0 6999 through df-9 7752) and the number 10 (df-10 7753) 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 9506. (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 7736 . 2 class 2
2 c1 6993 . . 3 class 1
3 caddc 6995 . . 3 class +
42, 2, 3co 4922 . 2 class (1 + 1)
51, 4wceq 1434 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re 7754  2pos 7765  1p1e2 7776  2p2e4 7777  2timesi 7778  3p2e5 7782  4p2e6 7784  5p2e7 7787  6p2e8 7791  7p2e9 7794  8p2e10 7796  2nn 7803  1lt2 7812  halfpos 7851  nneo 7982  eluz2b1 8090  fztp 8443  fzprval 8446  fztpval 8447  sqval 8676  fac2 8760  faclbnd4lem1 8771  bcp1m1 8795  hashpr 8822  binom11 9360  climcndslem1 9375  climcndslem2 9376  ege2le3 9429  ef4p 9450  efgt1p2 9451  efcnlem 9459  eirrlem 9520  odd2np1lem 9618  isprm3 9721  opoe 9774  pockthlem 9844  pockthg 9845  prmunb 9853  prmreclem2 9856  4sqlem19 9902  vdwlem12 9931  decexp2 9948  prmlem2 9964  83prm 9967  317prm 9970  1259lem2 9975  1259lem3 9976  1259lem4 9977  1259lem5 9978  2503lem1 9980  2503lem2 9981  2503lem3 9982  4001lem1 9984  4001lem2 9985  4001lem3 9986  4001lem4 9987  abvtriv 10392  vc2 11641  ipval2 11813  ip2i 11939  ovolunlem1 12110  ovolicc1lem 12123  vitalilem2 12179  itgcnlem 12359  coskpi 12695  ang180lem3 12760  emcllem7 12816  ppi2 12866  ppi3 12867  cht2 12868  ppieq0 12872  ppiublem 12875  chtublem 12878  chtub 12879  basellem3 12890  basellem5 12892  basellem8 12895  bcp1ctr 12902  bclbnd 12903  bposlem1 12907  bposlem2 12908  bposlem6 12912  ostthlem2 12942  1p1e2apr1 12957  hv2times 13102  pjthlem1 13433  ho2times 13862  stm1addi 14287  staddi 14288  stadd3i 14290  addltmulALT 14488  axlowdimlem4 15157  axlowdimlem13 15166  bpoly1 15370  bpolydiflem 15373  intset 16802
Copyright terms: Public domain