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

Theorem addid1d 10115
Description: 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
addid1d (𝜑 → (𝐴 + 0) = 𝐴)

Proof of Theorem addid1d
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addid1 10095 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  (class class class)co 6549  cc 9813  0cc0 9815   + caddc 9818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-ltxr 9958
This theorem is referenced by:  ltaddneg  10130  subsub2  10188  negsub  10208  ltaddpos  10397  addge01  10417  add20  10419  nnge1  10923  nnnn0addcl  11200  un0addcl  11203  uzaddcl  11620  xaddid1  11946  fzosubel3  12396  expadd  12764  faclbnd4lem4  12945  faclbnd6  12948  hashgadd  13027  ccatrid  13223  swrd0val  13273  swrdid  13280  swrd0fv  13291  swrd0swrd  13313  swrdccatin12lem2b  13337  swrdccatin12lem2  13340  swrdccat3blem  13346  splfv1  13357  cshweqrep  13418  relexpaddg  13641  reim0b  13707  rereb  13708  immul2  13725  max0add  13898  iseraltlem2  14261  fsumsplit  14318  sumsplit  14341  binomfallfaclem2  14610  pwp1fsum  14952  bitsinv1lem  15001  sadadd2lem2  15010  sadcaddlem  15017  bezoutlem1  15094  pcadd  15431  pcadd2  15432  pcmpt  15434  vdwapun  15516  vdwlem1  15523  mulgnn0dir  17394  psgnunilem2  17738  sylow1lem1  17836  efginvrel2  17963  efgredleme  17979  efgcpbllemb  17991  frgpnabllem1  18099  mplcoe5  19289  regsumfsum  19633  regsumsupp  19787  xrsxmet  22420  reparphti  22605  minveclem6  23013  ovolunnul  23075  voliunlem3  23127  ovolioo  23143  itg2splitlem  23321  itg2split  23322  itgrevallem1  23367  itgsplitioo  23410  ditgsplit  23431  dvnadd  23498  dvlipcn  23561  ply1divex  23700  dvntaylp  23929  ulmshft  23948  abelthlem6  23994  cosmpi  24044  sinppi  24045  sinhalfpip  24048  logrnaddcl  24125  affineequiv  24353  chordthmlem3  24361  atanlogaddlem  24440  atanlogsublem  24442  leibpi  24469  scvxcvx  24512  dmgmn0  24552  lgamgulmlem2  24556  lgambdd  24563  logexprlim  24750  2sqblem  24956  dchrvmasum2if  24986  dchrvmasumlem  25012  axcontlem8  25651  eupath2lem3  26506  ipidsq  26949  minvecolem6  27122  normpyc  27387  pjspansn  27820  lnfnmuli  28287  hstoh  28475  archirngz  29074  esumpfinvallem  29463  signsvtp  29986  signlem0  29990  cvxpcon  30478  cvxscon  30479  elmrsubrn  30671  faclim2  30887  fwddifn0  31441  fwddifnp1  31442  dnizeq0  31635  knoppndvlem6  31678  bj-bary1lem  32337  poimirlem1  32580  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem11  32590  poimirlem12  32591  poimirlem17  32596  poimirlem20  32599  poimirlem22  32601  poimirlem24  32603  poimirlem25  32604  poimirlem29  32608  poimirlem31  32610  mblfinlem2  32617  mbfposadd  32627  itg2addnc  32634  itgaddnclem2  32639  ftc1anclem5  32659  ftc1anclem8  32662  areacirc  32675  pell1qrgaplem  36455  jm2.19lem3  36576  jm2.25  36584  relexpaddss  37029  int-add01d  37509  binomcxplemnn0  37570  fperiodmullem  38458  xralrple3  38531  sumnnodd  38697  fprodaddrecnncnvlem  38796  ioodvbdlimc1lem2  38822  volioc  38864  volico  38876  stoweidlem11  38904  stoweidlem26  38919  stirlinglem12  38978  fourierdlem4  39004  fourierdlem42  39042  fourierdlem60  39059  fourierdlem61  39060  fourierdlem92  39091  fourierdlem107  39106  fouriersw  39124  etransclem24  39151  etransclem35  39162  hoidmvlelem2  39486  hspmbllem1  39516  sharhght  39703  deccarry  39941  pfxmpt  40250  pfxfv  40262  pfxccatin12lem1  40286  pfxccatin12lem2  40287  crctcshlem4  41023  eupth2lem3lem6  41401  altgsumbcALT  41924
  Copyright terms: Public domain W3C validator