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

Theorem addid2d 10835
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 10817 . 2 (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
31, 2syl 17 1 (𝜑 → (0 + 𝐴) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  (class class class)co 7146  cc 10529  0cc0 10531   + caddc 10534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4826  df-br 5054  df-opab 5116  df-mpt 5134  df-id 5448  df-po 5462  df-so 5463  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-ov 7149  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10671  df-mnf 10672  df-ltxr 10674
This theorem is referenced by:  negeu  10870  subge0  11147  sublt0d  11260  un0addcl  11925  lincmb01cmp  12880  ico01fl0  13191  discr  13604  ccatlid  13938  swrdfv0  14009  swrdpfx  14067  pfxpfx  14068  cats1un  14081  swrdccatin2  14089  cshwidx0mod  14165  cshw1  14182  relexpaddg  14410  rennim  14596  max0add  14668  fsumsplit  15095  sumsplit  15121  isumsplit  15193  arisum2  15214  binomfallfaclem2  15392  efaddlem  15444  eftlub  15460  ef4p  15464  rpnnen2lem11  15575  moddvds  15616  divalglem9  15748  sadadd2lem2  15795  sadcaddlem  15802  gcdmultipled  15878  pcmpt  16224  4sqlem11  16287  vdwlem6  16318  gsumsgrpccat  18002  gsumccatOLD  18003  mulgnn0dir  18255  sylow1lem1  18721  efgsval2  18857  efgsp1  18861  zaddablx  18990  pgpfaclem1  19201  mplcoe5  20244  regsumfsum  20608  regsumsupp  20761  nrmmetd  23179  blcvx  23401  xrsxmet  23412  reparphti  23600  nulmbl  24137  itg2splitlem  24350  itg2split  24351  itg2monolem1  24352  itgsplitioo  24439  ditgsplit  24462  dvcnp2  24521  dvcmul  24545  dvcmulf  24546  dvmptcmul  24565  dveflem  24580  dvef  24581  dvlipcn  24595  dvlt0  24606  plymullem1  24809  coeeulem  24819  dgradd2  24863  dgrmulc  24866  plydivlem3  24889  aareccl  24920  taylthlem1  24966  sin2kpi  25074  cos2kpi  25075  coshalfpim  25086  sinkpi  25112  chordthmlem3  25418  chordthmlem5  25420  dcubic1lem  25427  dcubic  25430  atancj  25494  atanlogaddlem  25497  atanlogsublem  25499  scvxcvx  25569  zetacvg  25598  ftalem5  25660  ftalem7  25662  basellem3  25666  chtublem  25793  2sqn0  26016  2sqnn  26021  rplogsumlem2  26067  dchrisumlem1  26071  pntrlog2bndlem2  26160  brbtwn2  26697  axlowdimlem16  26749  axeuclidlem  26754  elntg2  26777  eucrct2eupth  28028  2clwwlk2clwwlk  28133  bcm1n  30524  wrdt2ind  30633  esumpfinvallem  31360  signsplypnf  31847  fsum2dsub  31905  logdivsqrle  31948  revpfxsfxrev  32389  cvxpconn  32516  cvxsconn  32517  fwddifnp1  33653  tan2h  34961  poimirlem16  34985  mbfposadd  35016  itg2addnc  35023  ftc1anclem5  35046  bfplem2  35173  dffltz  39471  3cubeslem3r  39484  pellexlem6  39631  jm2.18  39785  sqrtcval  40197  relexpaddss  40275  int-add02d  40750  sub2times  41771  fzisoeu  41798  xralrple2  41852  cosknegpi  42377  dvsinax  42421  dvasinbx  42428  dvnxpaek  42450  dvnmul  42451  stoweidlem1  42509  stoweidlem13  42521  stoweidlem42  42550  stirlinglem5  42586  stirlinglem11  42592  fourierdlem42  42657  fourierdlem51  42665  fourierdlem88  42702  fourierdlem103  42717  fourierdlem104  42718  fourierdlem107  42721  sqwvfoura  42736  sqwvfourb  42737  fouriersw  42739  elaa2lem  42741  hspmbllem1  43131  cnambpcma  43717  readdcnnred  43726  nn0mnd  44305  altgsumbcALT  44620  nn0sumshdiglemA  44898  line2xlem  45021  line2x  45022  itschlc0yqe  45028  itsclc0yqsollem1  45030  itschlc0xyqsol1  45034  itschlc0xyqsol  45035  2itscp  45049
  Copyright terms: Public domain W3C validator