Theorem 00id 8469

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

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   0cc0 8180   + caddc 8183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8273  ax-icn 8275  ax-addcl 8276  ax-mulcl 8278  ax-i2m1 8285  ax-0id 8288

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  negdii  8612  addgt0  8778  addgegt0  8779  addgtge0  8780  addge0  8781  add20  8804  recexaplem2  8983  crap0  9291  iap0  9533  decaddm10  9845  10p10e20  9881  ser0  10985  bcpasc  11220  abs00ap  11844  fsumadd  12192  fsumrelem  12257  arisum  12284  bezoutr1  12829  nnnn0modprm0  13057  pcaddlem  13141  4sqlem19  13211  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem1  13265  1259lem2  13266  1259lem4  13268  cnfld0  14992  log2ublem3  16184  log2ublog2  16185  chtublem  16256  vtxdgfi0e  16702  1kp2ke3k  16904