Theorem 00id 8072

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 7924	. 2 ⊢ 0 ∈ ℂ
2		addid1 8069	. 2 ⊢ (0 ∈ ℂ → (0 + 0) = 0)
3	1, 2	ax-mp 5	1 ⊢ (0 + 0) = 0

Syntax hints:   = wceq 1353   ∈ wcel 2146  (class class class)co 5865  ℂcc 7784  0cc0 7786   + caddc 7789

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-ext 2157  ax-1cn 7879  ax-icn 7881  ax-addcl 7882  ax-mulcl 7884  ax-i2m1 7891  ax-0id 7894

This theorem depends on definitions:  df-bi 117  df-cleq 2168  df-clel 2171

This theorem is referenced by:  negdii  8215  addgt0  8379  addgegt0  8380  addgtge0  8381  addge0  8382  add20  8405  recexaplem2  8582  crap0  8888  iap0  9115  decaddm10  9415  10p10e20  9451  ser0  10484  bcpasc  10714  abs00ap  11039  fsumadd  11382  fsumrelem  11447  arisum  11474  bezoutr1  12001  nnnn0modprm0  12222  pcaddlem  12305  1kp2ke3k  14036