Theorem 00id 8474

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 8324	. 2 |- 0 e. CC
2		addrid 8471	. 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 6088   CCcc 8183   0cc0 8185   + caddc 8188

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 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-i2m1 8290  ax-0id 8293

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

This theorem is used by:  negdii  8617  addgt0  8783  addgegt0  8784  addgtge0  8785  addge0  8786  add20  8809  recexaplem2  8988  crap0  9296  iap0  9539  decaddm10  9851  10p10e20  9887  ser0  10991  bcpasc  11226  abs00ap  11850  fsumadd  12198  fsumrelem  12263  arisum  12290  bezoutr1  12835  nnnn0modprm0  13063  pcaddlem  13147  4sqlem19  13217  139prm  13267  163prm  13268  317prm  13269  631prm  13270  1259lem1  13271  1259lem2  13272  1259lem4  13274  cnfld0  15017  log2ublem3  16223  log2ublog2  16224  chtublem  16295  vtxdgfi0e  16741  1kp2ke3k  16943