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

Definition df-2 7706
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 6967 and df-1 6968).

Note: Only the digits 0 through 9 (df-0 6967 through df-9 7713) and the number 10 (df-10 7714) 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 9408. (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 7697 . 2 class 2
2 c1 6961 . . 3 class 1
3 caddc 6963 . . 3 class +
42, 2, 3co 4924 . 2 class (1 + 1)
51, 4wceq 1457 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re 7715  2pos 7726  1p1e2 7737  2p2e4 7738  2timesi 7739  3p2e5 7743  4p2e6 7745  5p2e7 7748  6p2e8 7752  7p2e9 7755  8p2e10 7757  2nn 7764  1lt2 7773  halfpos 7812  addltmul 7819  nneo 7941  zeo 7943  eluz2b1 8049  fztp 8394  fzprval 8397  fztpval 8398  sqval 8622  fac2 8706  faclbnd4lem1 8717  bcn2 8740  bcp1m1 8741  hashpr 8766  binom11 9236  ege2le3 9327  ef4p 9348  efcnlem 9357  cos2tsin 9399  cos2bnd 9408  eirrlem 9421  odd2np1lem 9516  isprm3 9619  2prm 9623  opoe 9672  pockthlem 9736  pockthg 9737  prmunb 9745  4sqlem18 9786  decexp2 9798  prmlem2 9814  83prm 9817  317prm 9820  1259lem2 9825  1259lem3 9826  1259lem4 9827  1259lem5 9828  2503lem1 9830  2503lem2 9831  2503lem3 9832  4001lem1 9834  4001lem2 9835  4001lem3 9836  4001lem4 9837  vc2 11426  ipval2 11599  ip2i 11725  cos2pi 11840  coskpi 11874  bcp1ctr 11930  bclbnd 11931  prmpiub 11934  prmor3 11935  prmorublem 11936  prmorub 11937  bposlem1 11940  bposlem2 11941  bposlem5 11944  1p1e2apr1 11952  hv2times 12097  pjthlem1 12428  ho2times 12857  stm1addi 13282  staddi 13283  stadd3i 13285  addltmulALT 13483  emcllem7 13503  ovolunlem1 13554  ovolicc1lem 13567  vitalilem2 13614  axlowdimlem4 14367  axlowdimlem13 14376  bpoly1 14580  bpolydiflem 14583  intset 16052
Copyright terms: Public domain