Definition df-2 5972

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 5253 and df-1 5254).

Note: Only the digits 0 through 9 (df-0 5253 through df-9 5979) and the number 10 (df-10 5980) 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 7476. (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 5963	. 2 class 2
2		c1 5247	. . 3 class 1
3		caddc 5249	. . 3 class +
4	2, 2, 3	co 3969	. 2 class (1 + 1)
5	1, 4	wceq 958	1 wff 2 = (1 + 1)

This definition is referenced by:  2re 5981  2pos 5991  2nn 6001  2p2e4 6003  2times 6005  3p2e5 6009  4p2e6 6011  5p2e7 6014  6p2e8 6018  7p2e9 6021  8p2e10 6023  1lt2 6030  halfpost 6038  nneo 6199  zeot 6201  sqvalt 6610  discrlem1 6657  fac2 6937  faclbnd4lem1 6948  fsum3 7024  ser1f0 7170  ege2lem2 7328  ege2le3lem2 7329  efaddlem8 7345  eirrlem1 7389  eirrlem3 7391  ef4p 7399  cos2tsint 7464  cos2bnd 7476  dscmet 7915  vc2 8170  ipval2 8353  ip2i 8483  cos2pi 8680  1p1e2 8782  hv2timest 8923  ho2timest 9740  stm1add 10167  stadd 10168  stadd3 10170

Copyright terms: Public domain