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

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

Note: Only the digits 0 through 9 (df-0 7007 through df-9 7759) and the number 10 (df-10 7760) 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 9458. (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 7743 . 2 class 2
2 c1 7001 . . 3 class 1
3 caddc 7003 . . 3 class +
42, 2, 3co 4931 . 2 class (1 + 1)
51, 4wceq 1449 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re 7761  2pos 7772  1p1e2 7783  2p2e4 7784  2timesi 7785  3p2e5 7789  4p2e6 7791  5p2e7 7794  6p2e8 7798  7p2e9 7801  8p2e10 7803  2nn 7810  1lt2 7819  halfpos 7858  nneo 7989  eluz2b1 8097  fztp 8449  fzprval 8452  fztpval 8453  sqval 8681  fac2 8765  faclbnd4lem1 8776  bcp1m1 8800  hashpr 8827  binom11 9314  climcndslem1 9329  climcndslem2 9330  ege2le3 9382  ef4p 9403  efcnlem 9411  eirrlem 9472  odd2np1lem 9569  isprm3 9672  opoe 9725  pockthlem 9795  pockthg 9796  prmunb 9804  prmreclem2 9807  4sqlem19 9853  vdwlem12 9882  decexp2 9899  prmlem2 9915  83prm 9918  317prm 9921  1259lem2 9926  1259lem3 9927  1259lem4 9928  1259lem5 9929  2503lem1 9931  2503lem2 9932  2503lem3 9933  4001lem1 9935  4001lem2 9936  4001lem3 9937  4001lem4 9938  abvtriv 10342  vc2 11590  ipval2 11762  ip2i 11888  ovolunlem1 12059  ovolicc1lem 12072  vitalilem2 12128  itgcnlem 12308  coskpi 12644  emcllem7 12739  basellem3 12753  basellem5 12755  basellem8 12758  bcp1ctr 12766  bclbnd 12767  prmpiub 12770  prmor3 12771  prmorublem 12772  prmorub 12773  bposlem1 12776  bposlem2 12777  bposlem6 12781  ostthlem2 12802  1p1e2apr1 12817  hv2times 12962  pjthlem1 13293  ho2times 13722  stm1addi 14147  staddi 14148  stadd3i 14150  addltmulALT 14348  axlowdimlem4 15017  axlowdimlem13 15026  bpoly1 15230  bpolydiflem 15233  intset 16662
Copyright terms: Public domain