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

Definition df-2 7816
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 7113 and df-1 7114).

Note: Only the digits 0 through 9 (df-0 7113 through df-9 7823) and the number 10 (df-10 7824) 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 9687. (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 7807 . 2 class 2
2 c1 7107 . . 3 class 1
3 caddc 7109 . . 3 class +
42, 2, 3co 5067 . 2 class (1 + 1)
51, 4wceq 1592 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re 7825  2pos 7836  2p2e4 7847  2timesi 7848  3p2e5 7852  4p2e6 7854  5p2e7 7857  6p2e8 7861  7p2e9 7864  8p2e10 7866  2nn 7873  1lt2 7882  halfpos 7921  addltmul 7928  nneoi 8111  zeo 8113  eluz2b1 8198  fztp 8529  fzprval 8532  fztpval 8533  sqval 8762  discrlem1 8823  fac2 9101  faclbnd4lem1 9112  hashpr 9155  fsum3 9213  binom11i 9266  ege2lem2 9529  ege2le3lem2 9530  efaddlem8 9546  eirrlem1 9590  eirrlem3 9592  ef4pi 9603  efgt1pi 9608  cos2tsin 9675  cos2bnd 9687  isprm3 9900  2prm 9904  prmunb 9924  dscmet 10778  vc2 11070  ipval2 11251  ip2i 11383  cos2pi 11560  coskpi 11590  1p1e2 11662  hv2times 12041  ho2times 12856  stm1addi 13279  staddi 13280  stadd3i 13282  addltmulALT 13480  pockthlem 13681  pockthg 13682  decexp2 13726  prmlem2 13742  83prm 13745  317prm 13748  1259lem2 13753  1259lem3 13754  1259lem4 13755  1259lem5 13756  2503lem1 13758  2503lem2 13759  2503lem3 13760  4001lem1 13762  4001lem2 13763  4001lem3 13764  4001lem4 13765  bclbnd 13772  bcp1ctr 13773  bclbnd2 13774  prmpiub 13777  prmor3 13778  prmorublem 13779  prmorub 13780  bposlem1 13783  bposlem2 13784  bposlem5 13787  axlowdimlem4 14414  axlowdimlem13 14423  axlowdimlem17 14427  intset 16014  mettrifi 16511  phtpyco 16691  pcoass 16720
Copyright terms: Public domain