Definition df-2 7487

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 6759 and df-1 6760).

Note: Only the digits 0 through 9 (df-0 6759 through df-9 7494) and the number 10 (df-10 7495) 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 9139. (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 7478	. 2 class 2
2		c1 6753	. . 3 class 1
3		caddc 6755	. . 3 class +
4	2, 2, 3	co 4981	. 2 class (1 + 1)
5	1, 4	wceq 1586	1 wff 2 = (1 + 1)

This definition is referenced by:  2re 7496  2pos 7506  2nn 7516  2p2e4 7518  2timesi 7520  3p2e5 7524  4p2e6 7526  5p2e7 7529  6p2e8 7533  7p2e9 7536  8p2e10 7538  1lt2 7547  halfpos 7562  addltmul 7569  nneoi 7752  zeo 7754  eluz2b1 7979  fztp 8049  fzprval 8050  fztpval 8051  sqval 8238  discrlem1 8290  fac2 8574  faclbnd4lem1 8585  fsum3 8680  ege2lem2 8988  ege2le3lem2 8989  efaddlem8 9005  eirrlem1 9049  eirrlem3 9051  ef4pi 9062  cos2tsin 9127  cos2bnd 9139  isprm3 9370  2prm 9374  prmunb 9392  dscmet 10062  vc2 10375  ipval2 10565  ip2i 10697  cos2pi 10905  coskpi 10935  1p1e2 11016  hv2times 11398  ho2times 12214  stm1addi 12648  staddi 12649  stadd3i 12651  addltmulALT 12849  mettrifi 16671  heiborlem30 16808  heiborlem32 16810  heiborlem33 16811  heiborlem35 16813  phtpyco 16880  pcoass 16909

Copyright terms: Public domain