Theorem 00id 8060

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

Syntax hints:   = wceq 1348   ∈ wcel 2141  (class class class)co 5853  ℂcc 7772  0cc0 7774   + caddc 7777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1cn 7867  ax-icn 7869  ax-addcl 7870  ax-mulcl 7872  ax-i2m1 7879  ax-0id 7882

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  negdii  8203  addgt0  8367  addgegt0  8368  addgtge0  8369  addge0  8370  add20  8393  recexaplem2  8570  crap0  8874  iap0  9101  decaddm10  9401  10p10e20  9437  ser0  10470  bcpasc  10700  abs00ap  11026  fsumadd  11369  fsumrelem  11434  arisum  11461  bezoutr1  11988  nnnn0modprm0  12209  pcaddlem  12292  1kp2ke3k  13759