Theorem 00id 8419

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

Syntax hints:   = wceq 1398   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130  0cc0 8132   + caddc 8135

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8225  ax-icn 8227  ax-addcl 8228  ax-mulcl 8230  ax-i2m1 8237  ax-0id 8240

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  negdii  8562  addgt0  8727  addgegt0  8728  addgtge0  8729  addge0  8730  add20  8753  recexaplem2  8931  crap0  9237  iap0  9466  decaddm10  9773  10p10e20  9809  ser0  10902  bcpasc  11136  abs00ap  11755  fsumadd  12100  fsumrelem  12165  arisum  12192  bezoutr1  12737  nnnn0modprm0  12961  pcaddlem  13045  4sqlem19  13115  cnfld0  14768  vtxdgfi0e  16339  1kp2ke3k  16541