Definition df-2 6031

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 5306 and df-1 5307).

Note: Only the digits 0 through 9 (df-0 5306 through df-9 6038) and the number 10 (df-10 6039) 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 7567. (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 6022	. 2 class 2
2		c1 5300	. . 3 class 1
3		caddc 5302	. . 3 class +
4	2, 2, 3	co 4021	. 2 class (1 + 1)
5	1, 4	wceq 997	1 wff 2 = (1 + 1)

This definition is referenced by:  2re 6040  2pos 6050  2nn 6060  2p2e4 6062  2timesi 6064  3p2e5 6068  4p2e6 6070  5p2e7 6073  6p2e8 6077  7p2e9 6080  8p2e10 6082  1lt2 6089  halfpos 6097  nneoi 6282  zeo 6284  sqval 6698  discrlem1 6746  fac2 7027  faclbnd4lem1 7038  fsum3 7114  ser1f0i 7260  ege2lem2 7418  ege2le3lem2 7419  efaddlem8 7435  eirrlem1 7479  eirrlem3 7481  ef4pi 7490  cos2tsin 7555  cos2bnd 7567  dscmet 8003  vc2 8258  ipval2 8441  ip2i 8571  cos2pi 8768  1p1e2 8870  hv2times 9011  ho2times 9828  stm1addi 10256  staddi 10257  stadd3i 10259

Copyright terms: Public domain