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

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

Note: Only the digits 0 through 9 (df-0 7014 through df-9 7767) and the number 10 (df-10 7768) 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 9521. (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 7751 . 2 class 2
2 c1 7008 . . 3 class 1
3 caddc 7010 . . 3 class +
42, 2, 3co 4927 . 2 class (1 + 1)
51, 4wceq 1434 1 wff 2 = (1 + 1)
Colors of variables: wff set class
This definition is referenced by:  2re 7769  2pos 7780  1p1e2 7791  2p2e4 7792  2timesi 7793  3p2e5 7797  4p2e6 7799  5p2e7 7802  6p2e8 7806  7p2e9 7809  8p2e10 7811  2nn 7818  1lt2 7827  halfpos 7866  nneo 7997  eluz2b1 8105  fztp 8458  fzprval 8461  fztpval 8462  sqval 8691  fac2 8775  faclbnd4lem1 8786  bcp1m1 8810  hashpr 8837  binom11 9375  climcndslem1 9390  climcndslem2 9391  ege2le3 9444  ef4p 9465  efgt1p2 9466  efcnlem 9474  eirrlem 9535  odd2np1lem 9633  isprm3 9736  opoe 9791  pockthlem 9861  pockthg 9862  prmunb 9870  prmreclem2 9873  4sqlem19 9919  vdwlem12 9948  decexp2 9965  prmlem2 9981  83prm 9984  317prm 9987  1259lem2 9992  1259lem3 9993  1259lem4 9994  1259lem5 9995  2503lem1 9997  2503lem2 9998  2503lem3 9999  4001lem1 10001  4001lem2 10002  4001lem3 10003  4001lem4 10004  abvtriv 10413  vc2 11663  ipval2 11835  ip2i 11961  ovolunlem1 12132  ovolicc1lem 12145  vitalilem2 12201  itgcnlem 12381  coskpi 12717  ang180lem3 12782  emcllem7 12838  ppi2 12888  ppi3 12889  cht2 12890  ppieq0 12894  ppiublem 12897  chtublem 12900  chtub 12901  basellem3 12912  basellem5 12914  basellem8 12917  bcp1ctr 12924  bclbnd 12925  bposlem1 12929  bposlem2 12930  bposlem6 12934  ostthlem2 12964  1p1e2apr1 12979  hv2times 13124  pjthlem1 13455  ho2times 13884  stm1addi 14309  staddi 14310  stadd3i 14312  addltmulALT 14510  axlowdimlem4 15179  axlowdimlem13 15188  bpoly1 15392  bpolydiflem 15395  intset 16824
Copyright terms: Public domain