Definition df-2 7589

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 6836 and df-1 6837).

Note: Only the digits 0 through 9 (df-0 6836 through df-9 7596) and the number 10 (df-10 7597) 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 9257. (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

Step	Hyp	Ref	Expression
1		c2 7580	. 2 class 2
2		c1 6830	. . 3 class 1
3		caddc 6832	. . 3 class +
4	2, 2, 3	co 5020	. 2 class (1 + 1)
5	1, 4	wceq 1615	1 wff 2 = (1 + 1)

This definition is referenced by:  2re 7598  2pos 7609  2nn 7620  2p2e4 7622  2timesi 7624  3p2e5 7628  4p2e6 7630  5p2e7 7633  6p2e8 7637  7p2e9 7640  8p2e10 7642  1lt2 7651  halfpos 7668  addltmul 7675  nneoi 7864  zeo 7866  eluz2b1 8093  fztp 8163  fzprval 8164  fztpval 8165  sqval 8354  discrlem1 8406  fac2 8690  faclbnd4lem1 8701  fsum3 8796  ege2lem2 9106  ege2le3lem2 9107  efaddlem8 9123  eirrlem1 9167  eirrlem3 9169  ef4pi 9180  cos2tsin 9245  cos2bnd 9257  isprm3 9506  2prm 9510  prmunb 9528  dscmet 10212  vc2 10527  ipval2 10717  ip2i 10851  cos2pi 11061  coskpi 11091  1p1e2 11174  hv2times 11556  ho2times 12372  stm1addi 12806  staddi 12807  stadd3i 12809  addltmulALT 13007  mettrifi 16932  heiborlem30 17069  heiborlem32 17071  heiborlem33 17072  heiborlem35 17074  phtpyco 17141  pcoass 17170

Copyright terms: Public domain