Definition df-2 4462

Description: Define the number 2.

Note that the numbers 0 and 1 are primitive constants of the complex number axiom system (see df-0 4035 and df-1 4036).

Note: The decimal representation of numbers will undergo a major revision at some point in the future, and the old rather clumsy development has been deleted. For now, every number that is needed should be exhibited as an explicit expression built from operations on the digits 0 through 9. For example, 350 can be expressed as ((7^3) + 7).

Assertion

Ref	Expression
df-2	|- 2 = (1 + 1)

Detailed syntax breakdown of Definition df-2

Step	Hyp	Ref	Expression
1		c2 4454	. 2 class 2
2		c1 4029	. . 3 class 1
3		caddc 4031	. . 3 class +
4	2, 2, 3	co 3001	. 2 class (1 + 1)
5	1, 4	wceq 1091	1 wff 2 = (1 + 1)

This definition is referenced by:  2re 4470  2pos 4479  2nn 4487  2p2e4 4488  2times 4489  3p2e5 4492  4p2e6 4494  5p2e7 4497  6p2e8 4500  7p2e9 4502  halfpost 4508  halfnz 4586  exp2t 4683  discrlem1 4713  nneo 4719  sqr2irrlem1 4777  ruclem25 4909  hv2times 5033  stm1add 5686  stadd 5687  stadd3 5689

metamath.org