Definition df-2 5868

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 5164 and df-1 5165).

Note: Only the digits 0 through 9 (df-0 5164 through df-9 5875) and the number 10 (df-10 5876) 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 7368. (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 5859	. 2 class 2
2		c1 5158	. . 3 class 1
3		caddc 5160	. . 3 class +
4	2, 2, 3	co 3902	. 2 class (1 + 1)
5	1, 4	wceq 1099	1 wff 2 = (1 + 1)

This definition is referenced by:  2re 5877  2pos 5887  2nn 5897  2p2e4 5899  2times 5901  3p2e5 5905  4p2e6 5907  5p2e7 5910  6p2e8 5914  7p2e9 5917  8p2e10 5919  1lt2 5926  halfpost 5934  nneo 6095  zeot 6097  sqvalt 6491  discrlem1 6537  fac2 6825  faclbnd4lem1 6836  fsum3 6913  ser1f0 7057  ege2lem2 7221  ege2le3lem2 7222  efaddlem8 7238  eirrlem1 7281  eirrlem3 7283  ef4p 7291  cos2bnd 7368  dscmet 7804  vc2 8061  ipval2 8226  ip2i 8353  cos2pi 8517  1p1e2 8967  hv2timest 9077  ho2timest 9876  stm1add 10296  stadd 10297  stadd3 10299

Copyright terms: Public domain