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

Theorem addid1d 9304
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 9284 . 2  |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( A  +  0 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1654    e. wcel 1728  (class class class)co 6117   CCcc 9026   0cc0 9028    + caddc 9031
This theorem is referenced by:  subsub2  9367  negsub  9387  ltaddpos  9556  addge01  9576  add20  9578  nnge1  10064  nnnn0addcl  10289  un0addcl  10291  uzaddcl  10571  xaddid1  10863  fzosubel3  11217  expadd  11460  faclbnd4lem4  11625  faclbnd6  11628  hashgadd  11689  ccatrid  11787  swrd0val  11806  swrdid  11810  splfv1  11822  reim0b  11962  rereb  11963  immul2  11980  max0add  12153  iseraltlem2  12514  fsumsplit  12571  sumsplit  12590  bitsinv1lem  12991  sadadd2lem2  13000  sadcaddlem  13007  bezoutlem1  13076  pcadd  13296  pcadd2  13297  pcmpt  13299  vdwapun  13380  vdwlem1  13387  mulgnn0dir  14951  sylow1lem1  15270  efginvrel2  15397  efgredleme  15413  efgcpbllemb  15425  frgpnabllem1  15522  mplcoe2  16568  xrsxmet  18878  reparphti  19060  minveclem6  19373  ovolunnul  19434  voliunlem3  19484  ovolioo  19500  itg2splitlem  19676  itg2split  19677  itgrevallem1  19722  itgsplitioo  19765  ditgsplit  19786  dvnadd  19853  dvlipcn  19916  ply1divex  20097  dvntaylp  20325  ulmshft  20344  abelthlem6  20390  cosmpi  20434  sinppi  20435  sinhalfpip  20438  logrnaddcl  20510  affineequiv  20705  chordthmlem3  20713  atanlogaddlem  20791  atanlogsublem  20793  leibpi  20820  scvxcvx  20862  logexprlim  21047  2sqblem  21199  dchrvmasum2if  21229  dchrvmasumlem  21255  eupath2lem3  21739  gxnn0add  21900  ipidsq  22247  minvecolem6  22422  normpyc  22686  pjspansn  23117  lnfnmuli  23585  hstoh  23773  esumpfinvallem  24499  dmgmn0  24845  lgamgulmlem2  24849  lgambdd  24856  cvxpcon  24964  cvxscon  24965  binomfallfaclem2  25391  faclim2  25402  axcontlem8  25945  mblfinlem2  26284  mbfposadd  26294  itg2addnc  26301  itgaddnclem2  26306  ftc1anclem5  26326  ftc1anclem8  26329  areacirc  26339  pell1qrgaplem  27048  jm2.19lem3  27174  jm2.25  27182  psgnunilem2  27507  stoweidlem11  27848  stoweidlem26  27863  stirlinglem12  27922  sharhght  27943  ubmelfzo  28247  swrd0fv  28324  swrdccatin12lem3b  28341  swrdccatin12lem3  28344  swrdccat3blem  28350  cshwidx  28374  cshweqrep  28406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736  ax-resscn 9085  ax-1cn 9086  ax-icn 9087  ax-addcl 9088  ax-addrcl 9089  ax-mulcl 9090  ax-mulrcl 9091  ax-mulcom 9092  ax-addass 9093  ax-mulass 9094  ax-distr 9095  ax-i2m1 9096  ax-1ne0 9097  ax-1rid 9098  ax-rnegex 9099  ax-rrecex 9100  ax-cnre 9101  ax-pre-lttri 9102  ax-pre-lttrn 9103  ax-pre-ltadd 9104
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-br 4244  df-opab 4298  df-mpt 4299  df-id 4533  df-po 4538  df-so 4539  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-fv 5497  df-ov 6120  df-er 6941  df-en 7146  df-dom 7147  df-sdom 7148  df-pnf 9160  df-mnf 9161  df-ltxr 9163
  Copyright terms: Public domain W3C validator