Definition df-2 5925

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 5221 and df-1 5222).

Note: Only the digits 0 through 9 (df-0 5221 through df-9 5932) and the number 10 (df-10 5933) 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 7425. (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 5916	. 2 class 2
2		c1 5215	. . 3 class 1
3		caddc 5217	. . 3 class +
4	2, 2, 3	co 3954	. 2 class (1 + 1)
5	1, 4	wceq 954	1 wff 2 = (1 + 1)

This definition is referenced by:  2re 5934  2pos 5944  2nn 5954  2p2e4 5956  2times 5958  3p2e5 5962  4p2e6 5964  5p2e7 5967  6p2e8 5971  7p2e9 5974  8p2e10 5976  1lt2 5983  halfpost 5991  nneo 6152  zeot 6154  sqvalt 6548  discrlem1 6594  fac2 6882  faclbnd4lem1 6893  fsum3 6970  ser1f0 7114  ege2lem2 7278  ege2le3lem2 7279  efaddlem8 7295  eirrlem1 7338  eirrlem3 7340  ef4p 7348  cos2bnd 7425  dscmet 7870  vc2 8126  ipval2 8304  ip2i 8431  cos2pi 8623  1p1e2 8726  hv2timest 8867  ho2timest 9685  stm1add 10110  stadd 10111  stadd3 10113

Copyright terms: Public domain