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

Definition df-2 7967
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 7219 and df-1 7220).

Note: Only the digits 0 through 9 (df-0 7219 through df-9 7974) and the number 10 (df-10 7975) 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 9803.

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

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 7958 . 2
2 c1 7213 . . 3
3 caddc 7215 . . 3
42, 2, 3co 5002 . 2
51, 4wceq 1414 1
Colors of variables: wff set class
This definition is referenced by:  2re 7976  2pos 7987  1p1e2 7998  2p2e4 7999  2timesi 8000  3p2e5 8004  4p2e6 8006  5p2e7 8009  6p2e8 8013  7p2e9 8016  8p2e10 8018  2nn 8025  1lt2 8034  halfpos 8087  nneo 8219  eluz2b1 8329  fztp 8689  fzprval 8692  fztpval 8693  sqval 8927  fac2 9011  faclbnd4lem1 9022  bcp1m1 9047  hashpr 9079  iseralt 9523  binom11 9644  climcndslem1 9659  climcndslem2 9660  ege2le3 9714  ef4p 9735  efgt1p2 9736  efcnlem 9744  eirrlem 9817  odd2np1lem 9918  isprm3 10022  opoe 10081  pockthlem 10155  pockthg 10156  prmunb 10164  prmreclem2 10167  4sqlem19 10213  vdwlem12 10242  decexp2 10259  prmlem2 10275  83prm 10278  317prm 10281  1259lem2 10286  1259lem3 10287  1259lem4 10288  1259lem5 10289  2503lem1 10291  2503lem2 10292  2503lem3 10293  4001lem1 10295  4001lem2 10296  4001lem3 10297  4001lem4 10298  abvtriv 11255  vc2 12873  ipval2 13045  ip2i 13171  ovolunlem1 13353  ovolicc1 13372  vitalilem2 13459  itgcnlem 13639  dveflem 13793  coskpi 14087  ang180lem3 14184  tanatan 14285  cosatan 14287  atantayl2 14304  emcllem7 14329  ppi2 14379  ppi3 14380  cht2 14381  ppieq0 14385  ppiublem 14388  chtublem 14391  chtub 14392  basellem3 14403  basellem5 14405  basellem8 14408  bcp1ctr 14415  bclbnd 14416  bposlem1 14420  bposlem2 14421  bposlem6 14425  ostthlem2 14452  1p1e2apr1 14467  hv2times 14628  pjthlem1 14959  ho2times 15388  stm1addi 15813  staddi 15814  stadd3i 15816  addltmulALT 16014  subfacp1lem1 16103  subfacp1lem5 16108  subfacp1lem6 16109  lgslem1 16137  lgsval2lem 16147  lgsdir2lem2 16165  lgsdir2lem3 16166  lgsdirprm 16170  hashprlei 16181  vdgr1d 16303  konigsberg 16323  axlowdimlem4 17211  axlowdimlem13 17220  bpoly1 17424  bpolydiflem 17427  intset 18839  pell14qrgapw 19945  rmydioph 20095  rmxdioph 20097  expdiophlem1 20102  expdiophlem2 20103  expdioph 20104
Copyright terms: Public domain