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

Definition df-2 7759
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 7013 and df-1 7014).

Note: Only the digits 0 through 9 (df-0 7013 through df-9 7766) and the number 10 (df-10 7767) 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 . Decimals can be expressed as ratios of integers, as in cos2bnd 9523. (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

Detailed syntax breakdown of Definition df-2
StepHypRef Expression
1 c2 7750 . 2
2 c1 7007 . . 3
3 caddc 7009 . . 3
42, 2, 3co 4924 . 2
51, 4wceq 1425 1
Colors of variables: wff set class
This definition is referenced by:  2re 7768  2pos 7779  1p1e2 7790  2p2e4 7791  2timesi 7792  3p2e5 7796  4p2e6 7798  5p2e7 7801  6p2e8 7805  7p2e9 7808  8p2e10 7810  2nn 7817  1lt2 7826  halfpos 7865  nneo 7996  eluz2b1 8104  fztp 8457  fzprval 8460  fztpval 8461  sqval 8691  fac2 8775  faclbnd4lem1 8786  bcp1m1 8810  hashpr 8837  binom11 9377  climcndslem1 9392  climcndslem2 9393  ege2le3 9446  ef4p 9467  efgt1p2 9468  efcnlem 9476  eirrlem 9537  odd2np1lem 9635  isprm3 9738  opoe 9793  pockthlem 9863  pockthg 9864  prmunb 9872  prmreclem2 9875  4sqlem19 9921  vdwlem12 9950  decexp2 9967  prmlem2 9983  83prm 9986  317prm 9989  1259lem2 9994  1259lem3 9995  1259lem4 9996  1259lem5 9997  2503lem1 9999  2503lem2 10000  2503lem3 10001  4001lem1 10003  4001lem2 10004  4001lem3 10005  4001lem4 10006  abvtriv 10415  vc2 11665  ipval2 11837  ip2i 11963  ovolunlem1 12134  ovolicc1lem 12147  vitalilem2 12203  itgcnlem 12383  coskpi 12719  ang180lem3 12784  emcllem7 12840  ppi2 12890  ppi3 12891  cht2 12892  ppieq0 12896  ppiublem 12899  chtublem 12902  chtub 12903  basellem3 12914  basellem5 12916  basellem8 12919  bcp1ctr 12926  bclbnd 12927  bposlem1 12931  bposlem2 12932  bposlem6 12936  ostthlem2 12966  1p1e2apr1 12981  hv2times 13126  pjthlem1 13457  ho2times 13886  stm1addi 14311  staddi 14312  stadd3i 14314  addltmulALT 14512  axlowdimlem4 15181  axlowdimlem13 15190  bpoly1 15394  bpolydiflem 15397  intset 16844  pell14qrgapw 17764  rmydioph 17915  rmxdioph 17917  expdiophlem1 17922  expdiophlem2 17923  expdioph 17924
Copyright terms: Public domain