Theorem 00id 7910

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

Syntax hints:   = wceq 1331   ∈ wcel 1480  (class class class)co 5774  ℂcc 7625  0cc0 7627   + caddc 7630

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1cn 7720  ax-icn 7722  ax-addcl 7723  ax-mulcl 7725  ax-i2m1 7732  ax-0id 7735

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  negdii  8053  addgt0  8217  addgegt0  8218  addgtge0  8219  addge0  8220  add20  8243  recexaplem2  8420  crap0  8723  iap0  8950  decaddm10  9247  10p10e20  9283  ser0  10294  bcpasc  10519  abs00ap  10841  fsumadd  11182  fsumrelem  11247  arisum  11274  bezoutr1  11728  1kp2ke3k  12946