MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addid2d Structured version   Visualization version   GIF version

Theorem addid2d 10427
Description: 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
addid2d (𝜑 → (0 + 𝐴) = 𝐴)

Proof of Theorem addid2d
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addid2 10409 . 2 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
31, 2syl 17 1 (𝜑 → (0 + 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  wcel 2137  (class class class)co 6811  cc 10124  0cc0 10126   + caddc 10129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-po 5185  df-so 5186  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-ov 6814  df-er 7909  df-en 8120  df-dom 8121  df-sdom 8122  df-pnf 10266  df-mnf 10267  df-ltxr 10269
This theorem is referenced by:  negeu  10461  subge0  10731  sublt0d  10843  un0addcl  11516  lincmb01cmp  12506  ico01fl0  12812  discr  13193  ccatlid  13556  swrdfv0  13622  swrdswrd0  13660  cats1un  13673  swrdccatin2  13685  cshwidx0mod  13749  cshw1  13766  relexpaddg  13990  rennim  14176  max0add  14247  fsumsplit  14668  sumsplit  14696  isumsplit  14769  arisum2  14790  binomfallfaclem2  14968  efaddlem  15020  eftlub  15036  ef4p  15040  rpnnen2lem11  15150  moddvds  15191  divalglem9  15324  sadadd2lem2  15372  sadcaddlem  15379  pcmpt  15796  4sqlem11  15859  vdwlem6  15890  gsumccat  17577  mulgnn0dir  17770  sylow1lem1  18211  efgsval2  18344  efgsp1  18348  zaddablx  18473  pgpfaclem1  18678  mplcoe5  19668  regsumfsum  20014  regsumsupp  20168  nrmmetd  22578  blcvx  22800  xrsxmet  22811  reparphti  22995  nulmbl  23501  itg2splitlem  23712  itg2split  23713  itg2monolem1  23714  itgsplitioo  23801  ditgsplit  23822  dvcnp2  23880  dvcmul  23904  dvcmulf  23905  dvmptcmul  23924  dveflem  23939  dvef  23940  dvlipcn  23954  dvlt0  23965  plymullem1  24167  coeeulem  24177  dgradd2  24221  dgrmulc  24224  plydivlem3  24247  aareccl  24278  taylthlem1  24324  sin2kpi  24432  cos2kpi  24433  coshalfpim  24444  sinkpi  24468  chordthmlem3  24758  chordthmlem5  24760  dcubic1lem  24767  dcubic  24770  atancj  24834  atanlogaddlem  24837  atanlogsublem  24839  scvxcvx  24909  zetacvg  24938  ftalem5  25000  ftalem7  25002  basellem3  25006  chtublem  25133  rplogsumlem2  25371  dchrisumlem1  25375  pntrlog2bndlem2  25464  brbtwn2  25982  axlowdimlem16  26034  axeuclidlem  26039  eucrct2eupth  27395  2clwwlk2clwwlk  27505  bcm1n  29861  2sqn0  29953  esumpfinvallem  30443  signsplypnf  30934  signstfvn  30953  fsum2dsub  30992  logdivsqrle  31035  cvxpconn  31529  cvxsconn  31530  fwddifnp1  32576  tan2h  33712  poimirlem16  33736  mbfposadd  33768  itg2addnc  33775  ftc1anclem5  33800  bfplem2  33933  pellexlem6  37898  jm2.18  38055  relexpaddss  38510  int-add02d  38988  sub2times  39982  fzisoeu  40011  xralrple2  40066  cosknegpi  40581  dvsinax  40628  dvasinbx  40636  dvnxpaek  40658  dvnmul  40659  stoweidlem1  40719  stoweidlem13  40731  stoweidlem42  40760  stirlinglem5  40796  stirlinglem11  40802  fourierdlem42  40867  fourierdlem51  40875  fourierdlem88  40912  fourierdlem103  40927  fourierdlem104  40928  fourierdlem107  40931  sqwvfoura  40946  sqwvfourb  40947  fouriersw  40949  elaa2lem  40951  hspmbllem1  41344  cnambpcma  41817  pfxpfx  41923  altgsumbcALT  42639  nn0sumshdiglemA  42921
  Copyright terms: Public domain W3C validator