ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  00id GIF version

Theorem 00id 7917
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
StepHypRef Expression
1 0cn 7772 . 2 0 ∈ ℂ
2 addid1 7914 . 2 (0 ∈ ℂ → (0 + 0) = 0)
31, 2ax-mp 5 1 (0 + 0) = 0
Colors of variables: wff set class
Syntax hints:   = wceq 1331  wcel 1480  (class class class)co 5774  cc 7632  0cc0 7634   + caddc 7637
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 7727  ax-icn 7729  ax-addcl 7730  ax-mulcl 7732  ax-i2m1 7739  ax-0id 7742
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  negdii  8060  addgt0  8224  addgegt0  8225  addgtge0  8226  addge0  8227  add20  8250  recexaplem2  8427  crap0  8730  iap0  8957  decaddm10  9254  10p10e20  9290  ser0  10301  bcpasc  10526  abs00ap  10848  fsumadd  11189  fsumrelem  11254  arisum  11281  bezoutr1  11734  1kp2ke3k  13043
  Copyright terms: Public domain W3C validator