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

Theorem addid2d 9769
Description:  0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
addid2d  |-  ( ph  ->  ( 0  +  A
)  =  A )

Proof of Theorem addid2d
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addid2 9751 . 2  |-  ( A  e.  CC  ->  (
0  +  A )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( 0  +  A
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    e. wcel 1762  (class class class)co 6275   CCcc 9479   0cc0 9481    + caddc 9484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-po 4793  df-so 4794  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-ov 6278  df-er 7301  df-en 7507  df-dom 7508  df-sdom 7509  df-pnf 9619  df-mnf 9620  df-ltxr 9622
This theorem is referenced by:  negeu  9799  subge0  10054  un0addcl  10818  lincmb01cmp  11652  addmodid  11992  discr  12258  ccatlid  12555  swrdspsleq  12623  swrdswrd0  12637  cats1un  12651  swrdccatin2  12662  cshwidx0mod  12725  cshw1  12740  rennim  13022  max0add  13093  fsumsplit  13511  sumsplit  13532  isumsplit  13604  arisum2  13624  efaddlem  13679  eftlub  13694  ef4p  13698  rpnnen2lem11  13808  moddvds  13843  divalglem9  13907  sadadd2lem2  13948  sadcaddlem  13955  pcmpt  14259  4sqlem11  14321  vdwlem6  14352  gsumccat  15825  mulgnn0dir  15958  sylow1lem1  16407  efgsval2  16540  efgsp1  16544  zaddablx  16660  pgpfaclem1  16915  mplcoe5  17895  mplcoe2OLD  17897  regsumsupp  18418  nrmmetd  20823  blcvx  21031  xrsxmet  21042  reparphti  21225  nulmbl  21674  itg2splitlem  21883  itg2split  21884  itg2monolem1  21885  itgsplitioo  21972  ditgsplit  21993  dvcnp2  22051  dvcmul  22075  dvcmulf  22076  dvmptcmul  22095  dveflem  22108  dvef  22109  dvlipcn  22123  dvlt0  22134  plymullem1  22339  coeeulem  22349  dgradd2  22392  dgrmulc  22395  plydivlem3  22418  aareccl  22449  taylthlem1  22495  sin2kpi  22602  cos2kpi  22603  coshalfpim  22614  sinkpi  22638  chordthmlem3  22886  chordthmlem5  22888  dcubic1lem  22895  dcubic  22898  atancj  22962  atanlogaddlem  22965  atanlogsublem  22967  scvxcvx  23036  ftalem5  23071  ftalem7  23073  basellem3  23077  chtublem  23207  rplogsumlem2  23391  dchrisumlem1  23395  pntrlog2bndlem2  23484  brbtwn2  23877  axlowdimlem16  23929  axeuclidlem  23934  bcm1n  27118  regsumfsum  27285  esumpfinvallem  27570  signsplypnf  27997  signstfvn  28016  zetacvg  28047  cvxpcon  28177  cvxscon  28178  binomfallfaclem2  28589  tan2h  29475  mbfposadd  29490  itg2addnc  29497  ftc1anclem5  29522  bfplem2  29773  pellexlem6  30225  jm2.18  30387  sub2times  30851  sublt0d  30891  fzisoeu  30896  cosknegpi  31024  dvsinax  31060  dvasinbx  31069  stoweidlem1  31120  stoweidlem13  31132  stoweidlem42  31161  stirlinglem5  31197  stirlinglem11  31203  fourierdlem42  31268  fourierdlem51  31277  fourierdlem88  31314  fourierdlem103  31329  fourierdlem104  31330  fourierdlem107  31333  sqwvfoura  31348  sqwvfourb  31349  fouriersw  31351  cnambpcma  31603  altgsumbcALT  31881  bj-flbi3  33554
  Copyright terms: Public domain W3C validator