Theorem 00id 8410

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

Syntax hints:   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121  0cc0 8123   + caddc 8126

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 2214  ax-1cn 8216  ax-icn 8218  ax-addcl 8219  ax-mulcl 8221  ax-i2m1 8228  ax-0id 8231

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  negdii  8553  addgt0  8718  addgegt0  8719  addgtge0  8720  addge0  8721  add20  8744  recexaplem2  8922  crap0  9228  iap0  9457  decaddm10  9763  10p10e20  9799  ser0  10891  bcpasc  11124  abs00ap  11740  fsumadd  12085  fsumrelem  12150  arisum  12177  bezoutr1  12722  nnnn0modprm0  12946  pcaddlem  13030  4sqlem19  13100  cnfld0  14706  vtxdgfi0e  16277  1kp2ke3k  16479