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  9850  10p10e20  9886  ser0  10990  bcpasc  11225  abs00ap  11849  fsumadd  12197  fsumrelem  12262  arisum  12289  bezoutr1  12834  nnnn0modprm0  13062  pcaddlem  13146  4sqlem19  13216  139prm  13266  163prm  13267  317prm  13268  631prm  13269  1259lem1  13270  1259lem2  13271  1259lem4  13273  cnfld0  15016  log2ublem3  16240  log2ublog2  16241  chtublem  16312  vtxdgfi0e  16758  1kp2ke3k  16960