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

Theorem addid1d 10436
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 10416 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145  (class class class)co 6791  cc 10134  0cc0 10136   + caddc 10139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-po 5170  df-so 5171  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-ov 6794  df-er 7894  df-en 8108  df-dom 8109  df-sdom 8110  df-pnf 10276  df-mnf 10277  df-ltxr 10279
This theorem is referenced by:  ltaddneg  10451  subsub2  10509  negsub  10529  ltaddpos  10718  addge01  10738  add20  10740  nnge1  11246  nnnn0addcl  11523  un0addcl  11526  uzaddcl  11944  xaddid1  12270  fzosubel3  12730  expadd  13102  faclbnd4lem4  13280  faclbnd6  13283  hashgadd  13361  ccatrid  13562  swrd0val  13622  swrdid  13630  swrd0fv  13641  swrd0swrd  13663  swrdccatin12lem2b  13688  swrdccatin12lem2  13691  swrdccat3blem  13697  splfv1  13708  cshweqrep  13769  relexpaddg  13994  reim0b  14060  rereb  14061  immul2  14078  max0add  14251  iseraltlem2  14614  fsumsplit  14672  sumsplit  14700  binomfallfaclem2  14970  pwp1fsum  15315  bitsinv1lem  15364  sadadd2lem2  15373  sadcaddlem  15380  bezoutlem1  15457  pcadd  15793  pcadd2  15794  pcmpt  15796  vdwapun  15878  vdwlem1  15885  mulgnn0dir  17772  psgnunilem2  18115  sylow1lem1  18213  efginvrel2  18340  efgredleme  18356  efgcpbllemb  18368  frgpnabllem1  18476  mplcoe5  19676  regsumfsum  20022  regsumsupp  20178  xrsxmet  22825  reparphti  23009  minveclem6  23417  ovolunnul  23481  voliunlem3  23533  ovolioo  23549  itg2splitlem  23728  itg2split  23729  itgrevallem1  23774  itgsplitioo  23817  ditgsplit  23838  dvnadd  23905  dvlipcn  23970  ply1divex  24109  dvntaylp  24338  ulmshft  24357  abelthlem6  24403  cosmpi  24454  sinppi  24455  sinhalfpip  24458  logrnaddcl  24535  affineequiv  24767  chordthmlem3  24775  atanlogaddlem  24854  atanlogsublem  24856  leibpi  24883  scvxcvx  24926  dmgmn0  24966  lgamgulmlem2  24970  lgambdd  24977  logexprlim  25164  2sqblem  25370  dchrvmasum2if  25400  dchrvmasumlem  25426  axcontlem8  26065  crctcshlem4  26941  eupth2lem3lem6  27406  ipidsq  27898  minvecolem6  28071  normpyc  28336  pjspansn  28769  lnfnmuli  29236  hstoh  29424  archirngz  30076  indsumin  30417  esumpfinvallem  30469  signsvtp  30993  signlem0  30997  fsum2dsub  31018  cvxpconn  31555  cvxsconn  31556  elmrsubrn  31748  faclim2  31965  fwddifn0  32601  fwddifnp1  32602  dnizeq0  32795  knoppndvlem6  32838  bj-bary1lem  33490  poimirlem1  33736  poimirlem5  33740  poimirlem6  33741  poimirlem7  33742  poimirlem11  33746  poimirlem12  33747  poimirlem17  33752  poimirlem20  33755  poimirlem22  33757  poimirlem24  33759  poimirlem25  33760  poimirlem29  33764  poimirlem31  33766  mblfinlem2  33773  mbfposadd  33782  itg2addnc  33789  itgaddnclem2  33794  ftc1anclem5  33814  ftc1anclem8  33817  areacirc  33830  pell1qrgaplem  37956  jm2.19lem3  38077  jm2.25  38085  relexpaddss  38529  int-add01d  39006  binomcxplemnn0  39067  fperiodmullem  40027  xralrple3  40099  sumnnodd  40373  fprodaddrecnncnvlem  40634  ioodvbdlimc1lem2  40658  volioc  40698  volico  40710  stoweidlem11  40738  stoweidlem26  40753  stirlinglem12  40812  fourierdlem4  40838  fourierdlem42  40876  fourierdlem60  40893  fourierdlem61  40894  fourierdlem92  40925  fourierdlem107  40940  fouriersw  40958  etransclem24  40985  etransclem35  40996  hoidmvlelem2  41323  hspmbllem1  41353  sharhght  41567  deccarry  41842  pfxmpt  41908  pfxfv  41920  pfxccatin12lem1  41944  pfxccatin12lem2  41945  altgsumbcALT  42652
  Copyright terms: Public domain W3C validator