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

Theorem addid1d 9250
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 9230 . 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 1652    e. wcel 1725  (class class class)co 6067   CCcc 8972   0cc0 8974    + caddc 8977
This theorem is referenced by:  subsub2  9313  negsub  9333  ltaddpos  9502  addge01  9522  add20  9524  nnge1  10010  nnnn0addcl  10235  un0addcl  10237  uzaddcl  10517  xaddid1  10809  fzosubel3  11162  expadd  11405  faclbnd4lem4  11570  faclbnd6  11573  hashgadd  11634  ccatrid  11732  swrd0val  11751  swrdid  11755  splfv1  11767  reim0b  11907  rereb  11908  immul2  11925  max0add  12098  iseraltlem2  12459  fsumsplit  12516  sumsplit  12535  bitsinv1lem  12936  sadadd2lem2  12945  sadcaddlem  12952  bezoutlem1  13021  pcadd  13241  pcadd2  13242  pcmpt  13244  vdwapun  13325  vdwlem1  13332  mulgnn0dir  14896  sylow1lem1  15215  efginvrel2  15342  efgredleme  15358  efgcpbllemb  15370  frgpnabllem1  15467  mplcoe2  16513  xrsxmet  18823  reparphti  19005  minveclem6  19318  ovolunnul  19379  voliunlem3  19429  ovolioo  19445  itg2splitlem  19623  itg2split  19624  itgrevallem1  19669  itgsplitioo  19712  ditgsplit  19731  dvnadd  19798  dvlipcn  19861  ply1divex  20042  dvntaylp  20270  ulmshft  20289  abelthlem6  20335  cosmpi  20379  sinppi  20380  sinhalfpip  20383  logrnaddcl  20455  affineequiv  20650  chordthmlem3  20658  atanlogaddlem  20736  atanlogsublem  20738  leibpi  20765  scvxcvx  20807  logexprlim  20992  2sqblem  21144  dchrvmasum2if  21174  dchrvmasumlem  21200  eupath2lem3  21684  gxnn0add  21845  ipidsq  22192  minvecolem6  22367  normpyc  22631  pjspansn  23062  lnfnmuli  23530  hstoh  23718  esumpfinvallem  24447  dmgmn0  24793  lgamgulmlem2  24797  lgambdd  24804  cvxpcon  24912  cvxscon  24913  binomfallfaclem2  25340  faclim2  25351  axcontlem8  25853  mblfinlem  26185  mbfposadd  26195  itg2addnc  26200  itgaddnclem2  26205  areacirc  26229  pell1qrgaplem  26868  jm2.19lem3  26994  jm2.25  27002  psgnunilem2  27328  stoweidlem11  27669  stoweidlem26  27684  stirlinglem12  27743  sharhght  27764  ubmelfzo  28028  swrdccatin12lem3b  28064  swrdccatin12lem3  28066  swrdccat3b  28073
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pow 4364  ax-pr 4390  ax-un 4687  ax-resscn 9031  ax-1cn 9032  ax-icn 9033  ax-addcl 9034  ax-addrcl 9035  ax-mulcl 9036  ax-mulrcl 9037  ax-mulcom 9038  ax-addass 9039  ax-mulass 9040  ax-distr 9041  ax-i2m1 9042  ax-1ne0 9043  ax-1rid 9044  ax-rnegex 9045  ax-rrecex 9046  ax-cnre 9047  ax-pre-lttri 9048  ax-pre-lttrn 9049  ax-pre-ltadd 9050
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-nel 2596  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-sbc 3149  df-csb 3239  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-pw 3788  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-opab 4254  df-mpt 4255  df-id 4485  df-po 4490  df-so 4491  df-xp 4870  df-rel 4871  df-cnv 4872  df-co 4873  df-dm 4874  df-rn 4875  df-res 4876  df-ima 4877  df-iota 5404  df-fun 5442  df-fn 5443  df-f 5444  df-f1 5445  df-fo 5446  df-f1o 5447  df-fv 5448  df-ov 6070  df-er 6891  df-en 7096  df-dom 7097  df-sdom 7098  df-pnf 9106  df-mnf 9107  df-ltxr 9109
  Copyright terms: Public domain W3C validator