Theorem 00id 8220

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

Syntax hints:   = wceq 1373   ∈ wcel 2177  (class class class)co 5951  ℂcc 7930  0cc0 7932   + caddc 7935

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188  ax-1cn 8025  ax-icn 8027  ax-addcl 8028  ax-mulcl 8030  ax-i2m1 8037  ax-0id 8040

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  negdii  8363  addgt0  8528  addgegt0  8529  addgtge0  8530  addge0  8531  add20  8554  recexaplem2  8732  crap0  9038  iap0  9267  decaddm10  9569  10p10e20  9605  ser0  10685  bcpasc  10918  abs00ap  11417  fsumadd  11761  fsumrelem  11826  arisum  11853  bezoutr1  12398  nnnn0modprm0  12622  pcaddlem  12706  4sqlem19  12776  cnfld0  14377  1kp2ke3k  15734