MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addid1d Unicode version

Theorem addid1d 9014
Description:  0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
addid1d  |-  ( ph  ->  ( A  +  0 )  =  A )

Proof of Theorem addid1d
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addid1 8994 . 2  |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
31, 2syl 15 1  |-  ( ph  ->  ( A  +  0 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    e. wcel 1686  (class class class)co 5860   CCcc 8737   0cc0 8739    + caddc 8742
This theorem is referenced by:  subsub2  9077  negsub  9097  ltaddpos  9266  addge01  9286  add20  9288  nnge1  9774  nnnn0addcl  9997  un0addcl  9999  uzaddcl  10277  xaddid1  10568  fzosubel3  10912  expadd  11146  faclbnd4lem4  11311  faclbnd6  11314  hashgadd  11361  ccatrid  11437  swrd0val  11456  swrdid  11460  splfv1  11472  reim0b  11606  rereb  11607  immul2  11624  max0add  11797  iseraltlem2  12157  fsumsplit  12214  sumsplit  12233  bitsinv1lem  12634  sadadd2lem2  12643  sadcaddlem  12650  bezoutlem1  12719  pcadd  12939  pcadd2  12940  pcmpt  12942  vdwapun  13023  vdwlem1  13030  mulgnn0dir  14592  sylow1lem1  14911  efginvrel2  15038  efgredleme  15054  efgcpbllemb  15066  frgpnabllem1  15163  mplcoe2  16213  xrsxmet  18317  reparphti  18497  minveclem6  18800  ovolunnul  18861  voliunlem3  18911  ovolioo  18927  itg2splitlem  19105  itg2split  19106  itgrevallem1  19151  itgsplitioo  19194  ditgsplit  19213  dvnadd  19280  dvlipcn  19343  ply1divex  19524  dvntaylp  19752  ulmshft  19771  abelthlem6  19814  cosmpi  19858  sinppi  19859  sinhalfpip  19862  logrnaddcl  19933  affineequiv  20125  chordthmlem3  20133  atanlogaddlem  20211  atanlogsublem  20213  leibpi  20240  scvxcvx  20282  logexprlim  20466  2sqblem  20618  dchrvmasum2if  20648  dchrvmasumlem  20674  gxnn0add  20943  ipidsq  21288  minvecolem6  21463  normpyc  21727  pjspansn  22158  lnfnmuli  22626  hstoh  22814  esumpfinvallem  23444  cvxpcon  23775  cvxscon  23776  eupath2lem3  23905  axcontlem8  24601  itg2addnc  24935  areacirc  24942  iintlem1  25621  pell1qrgaplem  26969  jm2.19lem3  27095  jm2.25  27103  psgnunilem2  27429  stirlinglem6  27839  stirlinglem12  27845  sharhght  27866
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-mulcom 8803  ax-addass 8804  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1ne0 8808  ax-1rid 8809  ax-rnegex 8810  ax-rrecex 8811  ax-cnre 8812  ax-pre-lttri 8813  ax-pre-lttrn 8814  ax-pre-ltadd 8815
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-po 4316  df-so 4317  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-er 6662  df-en 6866  df-dom 6867  df-sdom 6868  df-pnf 8871  df-mnf 8872  df-ltxr 8874
  Copyright terms: Public domain W3C validator