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

Definition df-2 7800
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 7096 and df-1 7097).

Note: Only the digits 0 through 9 (df-0 7096 through df-9 7807) and the number 10 (df-10 7808) 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 9672. (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 7791 . 2 class 2
2 c1 7090 . . 3 class 1
3 caddc 7092 . . 3 class +
42, 2, 3co 5050 . 2 class (1 + 1)
51, 4wceq 1573 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re 7809  2pos 7820  2p2e4 7831  2timesi 7832  3p2e5 7836  4p2e6 7838  5p2e7 7841  6p2e8 7845  7p2e9 7848  8p2e10 7850  2nn 7857  1lt2 7866  halfpos 7905  addltmul 7912  nneoi 8095  zeo 8097  eluz2b1 8182  fztp 8514  fzprval 8517  fztpval 8518  sqval 8747  discrlem1 8808  fac2 9086  faclbnd4lem1 9097  hashpr 9140  fsum3 9198  binom11i 9251  ege2lem2 9514  ege2le3lem2 9515  efaddlem8 9531  eirrlem1 9575  eirrlem3 9577  ef4pi 9588  efgt1pi 9593  cos2tsin 9660  cos2bnd 9672  isprm3 9885  2prm 9889  prmunb 9909  dscmet 10814  vc2 11106  ipval2 11287  ip2i 11419  cos2pi 11596  coskpi 11626  1p1e2 11698  hv2times 12078  ho2times 12893  stm1addi 13316  staddi 13317  stadd3i 13319  addltmulALT 13517  pockthlem 13718  pockthg 13719  decexp2 13763  prmlem2 13779  83prm 13782  317prm 13785  1259lem2 13790  1259lem3 13791  1259lem4 13792  1259lem5 13793  2503lem1 13795  2503lem2 13796  2503lem3 13797  4001lem1 13799  4001lem2 13800  4001lem3 13801  4001lem4 13802  bclbnd 13809  bcp1ctr 13810  bclbnd2 13811  prmpiub 13814  prmor3 13815  prmorublem 13816  prmorub 13817  bposlem1 13820  bposlem2 13821  bposlem5 13824  odd2np1lem 14050  opoe 14052  axlowdimlem4 14575  axlowdimlem13 14584  axlowdimlem17 14588  intset 16236  mettrifi 16733  phtpyco 16913  pcoass 16942
Copyright terms: Public domain