Theorem 00id 7774

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

Syntax hints:   = wceq 1299   ∈ wcel 1448  (class class class)co 5706  ℂcc 7498  0cc0 7500   + caddc 7503

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082  ax-1cn 7588  ax-icn 7590  ax-addcl 7591  ax-mulcl 7593  ax-i2m1 7600  ax-0id 7603

This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096

This theorem is referenced by:  negdii  7917  addgt0  8077  addgegt0  8078  addgtge0  8079  addge0  8080  add20  8103  recexaplem2  8274  crap0  8574  iap0  8795  decaddm10  9092  10p10e20  9128  ser0  10128  bcpasc  10353  abs00ap  10674  fsumadd  11014  fsumrelem  11079  arisum  11106  bezoutr1  11514  1kp2ke3k  12539