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

Theorem 00id 7774
 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 7630 . 2 0 ∈ ℂ
2 addid1 7771 . 2 (0 ∈ ℂ → (0 + 0) = 0)
31, 2ax-mp 7 1 (0 + 0) = 0
 Colors of variables: wff set class Syntax hints:   = wceq 1299   ∈ wcel 1448  (class class class)co 5706  ℂcc 7498  0cc0 7500   + caddc 7503 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082  ax-1cn 7588  ax-icn 7590  ax-addcl 7591  ax-mulcl 7593  ax-i2m1 7600  ax-0id 7603 This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096 This theorem is referenced by:  negdii  7917  addgt0  8077  addgegt0  8078  addgtge0  8079  addge0  8080  add20  8103  recexaplem2  8274  crap0  8574  iap0  8795  decaddm10  9092  10p10e20  9128  ser0  10128  bcpasc  10353  abs00ap  10674  fsumadd  11014  fsumrelem  11079  arisum  11106  bezoutr1  11514  1kp2ke3k  12539
 Copyright terms: Public domain W3C validator