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

Definition df-2 7923
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 7177 and df-1 7178).

Note: Only the digits 0 through 9 (df-0 7177 through df-9 7930) and the number 10 (df-10 7931) 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 9706.

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. Of course, there are exceptions. For larger numbers, base 4 representation has proved useful; see deccl 8182 and the theorems that follow it. See also 4001prm 10200 (4001 is prime) and the proof of bpos 13737.

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 7914 . 2
2 c1 7171 . . 3
3 caddc 7173 . . 3
42, 2, 3co 4979 . 2
51, 4wceq 1414 1
Colors of variables: wff set class
This definition is referenced by:  2re 7932  2pos 7943  1p1e2 7954  2p2e4 7955  2timesi 7956  3p2e5 7960  4p2e6 7962  5p2e7 7965  6p2e8 7969  7p2e9 7972  8p2e10 7974  2nn 7981  1lt2 7990  halfpos 8031  nneo 8163  eluz2b1 8271  fztp 8625  fzprval 8628  fztpval 8629  sqval 8861  fac2 8944  faclbnd4lem1 8955  bcp1m1 8980  hashpr 9010  binom11 9560  climcndslem1 9575  climcndslem2 9576  ege2le3 9629  ef4p 9650  efgt1p2 9651  efcnlem 9659  eirrlem 9720  odd2np1lem 9820  isprm3 9924  opoe 9983  pockthlem 10056  pockthg 10057  prmunb 10065  prmreclem2 10068  4sqlem19 10114  vdwlem12 10143  decexp2 10160  prmlem2 10176  83prm 10179  317prm 10182  1259lem2 10187  1259lem3 10188  1259lem4 10189  1259lem5 10190  2503lem1 10192  2503lem2 10193  2503lem3 10194  4001lem1 10196  4001lem2 10197  4001lem3 10198  4001lem4 10199  abvtriv 11099  vc2 12437  ipval2 12609  ip2i 12735  ovolunlem1 12906  ovolicc1lem 12919  vitalilem2 12975  itgcnlem 13155  dveflem 13304  coskpi 13516  ang180lem3 13581  emcllem7 13637  ppi2 13687  ppi3 13688  cht2 13689  ppieq0 13693  ppiublem 13696  chtublem 13699  chtub 13700  basellem3 13711  basellem5 13713  basellem8 13716  bcp1ctr 13723  bclbnd 13724  bposlem1 13728  bposlem2 13729  bposlem6 13733  ostthlem2 13760  1p1e2apr1 13775  hv2times 13936  pjthlem1 14267  ho2times 14696  stm1addi 15121  staddi 15122  stadd3i 15124  addltmulALT 15322  subfacp1lem1 15411  subfacp1lem5 15416  subfacp1lem6 15417  lgslem1 15445  lgsval2lem 15455  lgsdir2lem2 15473  lgsdir2lem3 15474  lgsdirprm 15478  hashprlei 15489  axlowdimlem4 16450  axlowdimlem13 16459  bpoly1 16663  bpolydiflem 16666  intset 18098  pell14qrgapw 19231  rmydioph 19382  rmxdioph 19384  expdiophlem1 19389  expdiophlem2 19390  expdioph 19391
Copyright terms: Public domain