Definition df-2 5917

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 5213 and df-1 5214).

Note: Only the digits 0 through 9 (df-0 5213 through df-9 5924) and the number 10 (df-10 5925) 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 7417. (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 5908	. 2 class 2
2		c1 5207	. . 3 class 1
3		caddc 5209	. . 3 class +
4	2, 2, 3	co 3948	. 2 class (1 + 1)
5	1, 4	wceq 953	1 wff 2 = (1 + 1)

This definition is referenced by:  2re 5926  2pos 5936  2nn 5946  2p2e4 5948  2times 5950  3p2e5 5954  4p2e6 5956  5p2e7 5959  6p2e8 5963  7p2e9 5966  8p2e10 5968  1lt2 5975  halfpost 5983  nneo 6144  zeot 6146  sqvalt 6540  discrlem1 6586  fac2 6874  faclbnd4lem1 6885  fsum3 6962  ser1f0 7106  ege2lem2 7270  ege2le3lem2 7271  efaddlem8 7287  eirrlem1 7330  eirrlem3 7332  ef4p 7340  cos2bnd 7417  dscmet 7856  vc2 8111  ipval2 8291  ip2i 8418  cos2pi 8604  1p1e2 8726  hv2timest 8849  ho2timest 9662  stm1add 10082  stadd 10083  stadd3 10085

Copyright terms: Public domain