Theorem 00id 8430

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 8282	. 2 |- 0 e. CC
2		addrid 8427	. 2 |- ( 0 e. CC -> ( 0 + 0 ) = 0 )
3	1, 2	ax-mp 5	1 |- ( 0 + 0 ) = 0

Syntax hints:   = wceq 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   0cc0 8143   + caddc 8146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-i2m1 8248  ax-0id 8251

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  negdii  8573  addgt0  8739  addgegt0  8740  addgtge0  8741  addge0  8742  add20  8765  recexaplem2  8943  crap0  9249  iap0  9478  decaddm10  9785  10p10e20  9821  ser0  10919  bcpasc  11153  abs00ap  11772  fsumadd  12117  fsumrelem  12182  arisum  12209  bezoutr1  12754  nnnn0modprm0  12978  pcaddlem  13062  4sqlem19  13132  cnfld0  14845  vtxdgfi0e  16416  1kp2ke3k  16618