Definition df-2 6949

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 6189 and df-1 6190).

Note: Only the digits 0 through 9 (df-0 6189 through df-9 6956) and the number 10 (df-10 6957) 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 8536. (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 6940	. 2 class 2
2		c1 6183	. . 3 class 1
3		caddc 6185	. . 3 class +
4	2, 2, 3	co 4695	. 2 class (1 + 1)
5	1, 4	wceq 1136	1 wff 2 = (1 + 1)

This definition is referenced by:  2re 6958  2pos 6968  2nn 6978  2p2e4 6980  2timesi 6982  3p2e5 6986  4p2e6 6988  5p2e7 6991  6p2e8 6995  7p2e9 6998  8p2e10 7000  1lt2 7007  halfpos 7017  addltmul 7024  nneoi 7204  zeo 7206  fztp 7481  fzprval 7482  fztpval 7483  sqval 7649  discrlem1 7701  fac2 7984  faclbnd4lem1 7995  fsum3 8079  ege2lem2 8385  ege2le3lem2 8386  efaddlem8 8402  eirrlem1 8446  eirrlem3 8448  ef4pi 8459  cos2tsin 8524  cos2bnd 8536  dscmet 8991  vc2 9301  ipval2 9491  ip2i 9623  cos2pi 9829  coskpi 9859  1p1e2 9940  hv2times 10352  ho2times 11174  stm1addi 11609  staddi 11610  stadd3i 11612  addltmulALT 11810  mettrifi 15529  heiborlem30 15666  heiborlem32 15668  heiborlem33 15669  heiborlem35 15671  phtpyco 15738  pcoass 15767  stb2xpl 16501  stb3xpl 16502

Copyright terms: Public domain