Theorem 00id 8047

Description: 0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
00id	|- ( 0 + 0 ) = 0

Proof of Theorem 00id

Step	Hyp	Ref	Expression
1		0cn 7899	. 2 |- 0 e. CC
2		addid1 8044	. 2 |- ( 0 e. CC -> ( 0 + 0 ) = 0 )
3	1, 2	ax-mp 5	1 |- ( 0 + 0 ) = 0

Syntax hints:   = wceq 1348   e. wcel 2141  (class class class)co 5850   CCcc 7759   0cc0 7761   + caddc 7764

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1cn 7854  ax-icn 7856  ax-addcl 7857  ax-mulcl 7859  ax-i2m1 7866  ax-0id 7869

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  negdii  8190  addgt0  8354  addgegt0  8355  addgtge0  8356  addge0  8357  add20  8380  recexaplem2  8557  crap0  8861  iap0  9088  decaddm10  9388  10p10e20  9424  ser0  10457  bcpasc  10687  abs00ap  11013  fsumadd  11356  fsumrelem  11421  arisum  11448  bezoutr1  11975  nnnn0modprm0  12196  pcaddlem  12279  1kp2ke3k  13680