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

Theorem addid2d 11357
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 11339 . 2 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
31, 2syl 17 1 (𝜑 → (0 + 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  (class class class)co 7358  cc 11050  0cc0 11052   + caddc 11055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-po 5546  df-so 5547  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-ltxr 11195
This theorem is referenced by:  negeu  11392  subge0  11669  sublt0d  11782  un0addcl  12447  lincmb01cmp  13413  ico01fl0  13725  discr  14144  ccatlid  14475  swrdfv0  14538  swrdpfx  14596  pfxpfx  14597  cats1un  14610  swrdccatin2  14618  cshwidx0mod  14694  cshw1  14711  relexpaddg  14939  rennim  15125  max0add  15196  fsumsplit  15627  sumsplit  15654  isumsplit  15726  arisum2  15747  binomfallfaclem2  15924  efaddlem  15976  eftlub  15992  ef4p  15996  rpnnen2lem11  16107  moddvds  16148  divalglem9  16284  sadadd2lem2  16331  sadcaddlem  16338  gcdmultipled  16416  pcmpt  16765  4sqlem11  16828  vdwlem6  16859  gsumsgrpccat  18651  mulgnn0dir  18907  sylow1lem1  19381  efgsval2  19516  efgsp1  19520  zaddablx  19651  pgpfaclem1  19861  regsumfsum  20868  regsumsupp  21029  mplcoe5  21444  nrmmetd  23933  blcvx  24164  xrsxmet  24175  reparphti  24363  nulmbl  24902  itg2splitlem  25116  itg2split  25117  itg2monolem1  25118  itgsplitioo  25205  ditgsplit  25228  dvcnp2  25287  dvcmul  25311  dvcmulf  25312  dvmptcmul  25331  dveflem  25346  dvef  25347  dvlipcn  25361  dvlt0  25372  plymullem1  25578  coeeulem  25588  dgradd2  25632  dgrmulc  25635  plydivlem3  25658  aareccl  25689  taylthlem1  25735  sin2kpi  25843  cos2kpi  25844  coshalfpim  25855  sinkpi  25881  chordthmlem3  26187  chordthmlem5  26189  dcubic1lem  26196  dcubic  26199  atancj  26263  atanlogaddlem  26266  atanlogsublem  26268  scvxcvx  26338  zetacvg  26367  ftalem5  26429  ftalem7  26431  basellem3  26435  chtublem  26562  2sqn0  26785  2sqnn  26790  rplogsumlem2  26836  dchrisumlem1  26840  pntrlog2bndlem2  26929  brbtwn2  27857  axlowdimlem16  27909  axeuclidlem  27914  elntg2  27937  eucrct2eupth  29192  2clwwlk2clwwlk  29297  bcm1n  31701  wrdt2ind  31810  esumpfinvallem  32676  signsplypnf  33165  fsum2dsub  33223  logdivsqrle  33266  revpfxsfxrev  33712  cvxpconn  33839  cvxsconn  33840  fwddifnp1  34753  tan2h  36073  poimirlem16  36097  mbfposadd  36128  itg2addnc  36135  ftc1anclem5  36158  bfplem2  36285  aks4d1p1p4  40531  aks4d1p7d1  40542  sticksstones10  40566  sticksstones22  40579  dffltz  40975  3cubeslem3r  41013  pellexlem6  41160  jm2.18  41315  sqrtcval  41920  relexpaddss  41997  int-add02d  42465  sub2times  43513  fzisoeu  43541  xralrple2  43595  cosknegpi  44117  dvsinax  44161  dvasinbx  44168  dvnxpaek  44190  dvnmul  44191  stoweidlem1  44249  stoweidlem13  44261  stoweidlem42  44290  stirlinglem5  44326  stirlinglem11  44332  fourierdlem42  44397  fourierdlem51  44405  fourierdlem88  44442  fourierdlem103  44457  fourierdlem104  44458  fourierdlem107  44461  sqwvfoura  44476  sqwvfourb  44477  fouriersw  44479  elaa2lem  44481  hspmbllem1  44874  cnambpcma  45533  readdcnnred  45542  nn0mnd  46120  altgsumbcALT  46436  nn0sumshdiglemA  46712  line2xlem  46846  line2x  46847  itschlc0yqe  46853  itsclc0yqsollem1  46855  itschlc0xyqsol1  46859  itschlc0xyqsol  46860  2itscp  46874
  Copyright terms: Public domain W3C validator