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

Definition df-2 8020
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 7264 and df-1 7265).

Note: Only the digits 0 through 9 (df-0 7264 through df-9 8027) and the number 10 (df-10 8028) 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 9953.

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 8318 and the theorems that follow it. See also 4001prm 10491 (4001 is prime) and the proof of bpos 14722.

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 8011 . 2
2 c1 7258 . . 3
3 caddc 7260 . . 3
42, 2, 3co 5032 . 2
51, 4wceq 1414 1
Colors of variables: wff set class
This definition is referenced by:  2re 8029  2pos 8040  1p1e2 8051  2p2e4 8052  2timesi 8053  3p2e5 8065  4p2e6 8067  5p2e7 8070  6p2e8 8074  7p2e9 8077  8p2e10 8079  2nn 8086  1lt2 8095  halfpos 8148  nneo 8285  6p6e12 8355  7p5e12 8357  8p4e12 8361  9p2e11 8366  9p3e12 8367  eluz2b1 8469  fztp 8830  fzprval 8833  fztpval 8834  sqval 9068  fac2 9153  faclbnd4lem1 9164  bcp1m1 9189  hashpr 9222  iseralt 9671  binom11 9793  climcndslem1 9808  climcndslem2 9809  ege2le3 9864  ef4p 9885  efgt1p2 9886  efcnlem 9894  eirrlem 9967  odd2np1lem 10068  isprm3 10173  opoe 10232  pockthlem 10306  pockthg 10307  prmunb 10315  prmreclem2 10318  4sqlem19 10364  vdwlem12 10393  decexp2 10444  abvtrivd 11499  vc2 13128  ipval2 13300  ip2i 13426  ovolunlem1 13603  ovolicc1 13622  vitalilem2 13709  itgcnlem 13889  dveflem 14044  coskpi 14338  ang180lem3 14443  tanatan 14568  cosatan 14570  atantayl2 14587  emcllem7 14622  basellem3 14636  basellem5 14638  basellem8 14641  ppi2 14690  ppi3 14691  cht2 14692  ppieq0 14696  ppiublem 14699  chtublem 14702  chtub 14703  bcp1ctr 14708  bclbnd 14709  bposlem1 14713  bposlem2 14714  bposlem6 14718  ostthlem2 14745  1p1e2apr1 14768  hv2times 15145  pjthlem1 15476  ho2times 15905  stm1addi 16330  staddi 16331  stadd3i 16333  addltmulALT 16531  subfacp1lem1 16621  subfacp1lem5 16626  subfacp1lem6 16627  lgslem1 16655  lgsval2lem 16665  lgsdir2lem2 16683  lgsdir2lem3 16684  lgsdirprm 16688  vdgr1d 16821  konigsberg 16841  axlowdimlem4 17525  axlowdimlem13 17534  bpoly1 17738  bpolydiflem 17741  intset 19151  pell14qrgapw 20346  rmydioph 20496  rmxdioph 20498  expdiophlem1 20503  expdiophlem2 20504  expdioph 20505
Copyright terms: Public domain