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

Theorem addid1d 9779
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 9759 . 2  |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
31, 2syl 17 1  |-  ( ph  ->  ( A  +  0 )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1872  (class class class)co 6244   CCcc 9483   0cc0 9485    + caddc 9488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-po 4712  df-so 4713  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-ov 6247  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-ltxr 9626
This theorem is referenced by:  subsub2  9848  negsub  9868  ltaddpos  10050  addge01  10070  add20  10072  nnge1  10581  nnnn0addcl  10846  un0addcl  10849  uzaddcl  11161  xaddid1  11478  fzosubel3  11920  expadd  12259  faclbnd4lem4  12426  faclbnd6  12429  hashgadd  12501  ccatrid  12674  swrd0val  12718  swrdid  12725  swrd0fv  12736  swrd0swrd  12758  swrdccatin12lem2b  12783  swrdccatin12lem2  12786  swrdccat3blem  12792  splfv1  12803  cshweqrep  12861  relexpaddg  13055  reim0b  13121  rereb  13122  immul2  13139  max0add  13312  iseraltlem2  13687  fsumsplit  13744  sumsplit  13767  binomfallfaclem2  14031  bitsinv1lem  14353  sadadd2lem2  14362  sadcaddlem  14369  bezoutlem1  14441  pcadd  14772  pcadd2  14773  pcmpt  14775  vdwapun  14862  vdwlem1  14869  mulgnn0dir  16719  psgnunilem2  17074  sylow1lem1  17188  efginvrel2  17315  efgredleme  17331  efgcpbllemb  17343  frgpnabllem1  17447  mplcoe5  18630  regsumsupp  19127  xrsxmet  21764  reparphti  21965  minveclem6  22313  minveclem6OLD  22325  ovolunnul  22390  voliunlem3  22442  ovolioo  22458  itg2splitlem  22643  itg2split  22644  itgrevallem1  22689  itgsplitioo  22732  ditgsplit  22753  dvnadd  22820  dvlipcn  22883  ply1divex  23024  dvntaylp  23263  ulmshft  23282  abelthlem6  23328  cosmpi  23380  sinppi  23381  sinhalfpip  23384  logrnaddcl  23461  affineequiv  23689  chordthmlem3  23697  atanlogaddlem  23776  atanlogsublem  23778  leibpi  23805  scvxcvx  23848  dmgmn0  23888  lgamgulmlem2  23892  lgambdd  23899  logexprlim  24090  2sqblem  24242  dchrvmasum2if  24272  dchrvmasumlem  24298  axcontlem8  24938  eupath2lem3  25644  gxnn0add  25939  ipidsq  26286  minvecolem6  26461  minvecolem6OLD  26471  normpyc  26736  pjspansn  27167  lnfnmuli  27634  hstoh  27822  archirngz  28452  regsumfsum  28491  esumpfinvallem  28842  signsvtp  29419  signlem0  29423  cvxpcon  29912  cvxscon  29913  elmrsubrn  30105  faclim2  30330  fwddifn0  30875  fwddifnp1  30876  bj-bary1lem  31622  poimirlem1  31848  poimirlem5  31852  poimirlem6  31853  poimirlem7  31854  poimirlem11  31858  poimirlem12  31859  poimirlem17  31864  poimirlem20  31867  poimirlem22  31869  poimirlem24  31871  poimirlem25  31872  poimirlem29  31876  poimirlem31  31878  mblfinlem2  31885  mbfposadd  31895  itg2addnc  31903  itgaddnclem2  31908  ftc1anclem5  31928  ftc1anclem8  31931  areacirc  31944  pell1qrgaplem  35632  jm2.19lem3  35759  jm2.25  35767  relexpaddss  36223  int-add01d  36544  binomcxplemnn0  36611  ltaddneg  37405  fperiodmullem  37418  sumnnodd  37593  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  volioc  37732  stoweidlem11  37754  stoweidlem26  37769  stirlinglem12  37830  fourierdlem4  37856  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem60  37913  fourierdlem61  37914  fourierdlem92  37945  fourierdlem107  37960  fouriersw  37978  etransclem24  38006  etransclem35  38017  volico  38210  hoidmvlelem2  38265  sharhght  38288  deccarry  38528  pfxmpt  38741  pfxfv  38753  pfxccatin12lem1  38777  pfxccatin12lem2  38778  altgsumbcALT  39727
  Copyright terms: Public domain W3C validator