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

Definition df-2 7775
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 7029 and df-1 7030).

Note: Only the digits 0 through 9 (df-0 7029 through df-9 7782) and the number 10 (df-10 7783) 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 9541. (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 7766 . 2
2 c1 7023 . . 3
3 caddc 7025 . . 3
42, 2, 3co 4931 . 2
51, 4wceq 1425 1
Colors of variables: wff set class
This definition is referenced by:  2re 7784  2pos 7795  1p1e2 7806  2p2e4 7807  2timesi 7808  3p2e5 7812  4p2e6 7814  5p2e7 7817  6p2e8 7821  7p2e9 7824  8p2e10 7826  2nn 7833  1lt2 7842  halfpos 7881  nneo 8012  eluz2b1 8120  fztp 8473  fzprval 8476  fztpval 8477  sqval 8708  fac2 8792  faclbnd4lem1 8803  bcp1m1 8827  hashpr 8854  binom11 9395  climcndslem1 9410  climcndslem2 9411  ege2le3 9464  ef4p 9485  efgt1p2 9486  efcnlem 9494  eirrlem 9555  odd2np1lem 9653  isprm3 9756  opoe 9811  pockthlem 9881  pockthg 9882  prmunb 9890  prmreclem2 9893  4sqlem19 9939  vdwlem12 9968  decexp2 9985  prmlem2 10001  83prm 10004  317prm 10007  1259lem2 10012  1259lem3 10013  1259lem4 10014  1259lem5 10015  2503lem1 10017  2503lem2 10018  2503lem3 10019  4001lem1 10021  4001lem2 10022  4001lem3 10023  4001lem4 10024  abvtriv 10678  vc2 11931  ipval2 12103  ip2i 12229  ovolunlem1 12400  ovolicc1lem 12413  vitalilem2 12469  itgcnlem 12649  coskpi 12985  ang180lem3 13050  emcllem7 13106  ppi2 13156  ppi3 13157  cht2 13158  ppieq0 13162  ppiublem 13165  chtublem 13168  chtub 13169  basellem3 13180  basellem5 13182  basellem8 13185  bcp1ctr 13192  bclbnd 13193  bposlem1 13197  bposlem2 13198  bposlem6 13202  ostthlem2 13229  1p1e2apr1 13244  hv2times 13395  pjthlem1 13726  ho2times 14155  stm1addi 14580  staddi 14581  stadd3i 14583  addltmulALT 14781  axlowdimlem4 15574  axlowdimlem13 15583  bpoly1 15787  bpolydiflem 15790  intset 17237  pell14qrgapw 18156  rmydioph 18307  rmxdioph 18309  expdiophlem1 18314  expdiophlem2 18315  expdioph 18316
Copyright terms: Public domain