Definition df-2 5979

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 5260 and df-1 5261).

Note: Only the digits 0 through 9 (df-0 5260 through df-9 5986) and the number 10 (df-10 5987) 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 7483. (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 5970	. 2 class 2
2		c1 5254	. . 3 class 1
3		caddc 5256	. . 3 class +
4	2, 2, 3	co 3970	. 2 class (1 + 1)
5	1, 4	wceq 958	1 wff 2 = (1 + 1)

This definition is referenced by:  2re 5988  2pos 5998  2nn 6008  2p2e4 6010  2times 6012  3p2e5 6016  4p2e6 6018  5p2e7 6021  6p2e8 6025  7p2e9 6028  8p2e10 6030  1lt2 6037  halfpost 6045  nneo 6206  zeot 6208  sqvalt 6617  discrlem1 6664  fac2 6944  faclbnd4lem1 6955  fsum3 7031  ser1f0 7177  ege2lem2 7335  ege2le3lem2 7336  efaddlem8 7352  eirrlem1 7396  eirrlem3 7398  ef4p 7406  cos2tsint 7471  cos2bnd 7483  dscmet 7922  vc2 8177  ipval2 8360  ip2i 8490  cos2pi 8687  1p1e2 8789  hv2timest 8930  ho2timest 9747  stm1add 10175  stadd 10176  stadd3 10178

Copyright terms: Public domain