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

Theorem 00id 7910
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 7765 . 2  |-  0  e.  CC
2 addid1 7907 . 2  |-  ( 0  e.  CC  ->  (
0  +  0 )  =  0 )
31, 2ax-mp 5 1  |-  ( 0  +  0 )  =  0
Colors of variables: wff set class
Syntax hints:    = wceq 1331    e. wcel 1480  (class class class)co 5774   CCcc 7625   0cc0 7627    + caddc 7630
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 7720  ax-icn 7722  ax-addcl 7723  ax-mulcl 7725  ax-i2m1 7732  ax-0id 7735
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  negdii  8053  addgt0  8217  addgegt0  8218  addgtge0  8219  addge0  8220  add20  8243  recexaplem2  8420  crap0  8723  iap0  8950  decaddm10  9247  10p10e20  9283  ser0  10294  bcpasc  10519  abs00ap  10841  fsumadd  11182  fsumrelem  11247  arisum  11274  bezoutr1  11728  1kp2ke3k  12950
  Copyright terms: Public domain W3C validator