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

Theorem addid1d 10490
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 10470 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wcel 2155  (class class class)co 6842  cc 10187  0cc0 10189   + caddc 10192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-po 5198  df-so 5199  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-ltxr 10333
This theorem is referenced by:  ltaddneg  10505  subsub2  10563  negsub  10583  ltaddpos  10772  addge01  10792  add20  10794  nnge1  11303  nnnn0addcl  11570  un0addcl  11573  uzaddcl  11944  xaddid1  12274  fzosubel3  12737  expadd  13109  faclbnd4lem4  13287  faclbnd6  13290  hashgadd  13368  ccatrid  13558  swrd0valOLD  13622  swrdidOLD  13630  swrd0fvOLD  13641  pfxmpt  13667  pfxfv  13671  swrd0swrdOLD  13693  pfxswrd  13694  pfxccatin12lem1  13732  swrdccatin12lem2bOLD  13733  pfxccatin12lem2  13736  swrdccatin12lem2OLD  13737  swrdccat3blem  13749  splfv1OLD  13777  cshweqrep  13850  relexpaddg  14078  reim0b  14144  rereb  14145  immul2  14162  max0add  14335  iseraltlem2  14698  fsumsplit  14756  sumsplit  14784  binomfallfaclem2  15053  pwp1fsum  15396  bitsinv1lem  15444  sadadd2lem2  15453  sadcaddlem  15460  bezoutlem1  15537  pcadd  15872  pcadd2  15873  pcmpt  15875  vdwapun  15957  vdwlem1  15964  mulgnn0dir  17836  psgnunilem2  18179  sylow1lem1  18277  efginvrel2  18404  efgredleme  18421  efgcpbllemb  18434  frgpnabllem1  18542  mplcoe5  19742  regsumfsum  20087  regsumsupp  20242  xrsxmet  22891  reparphti  23075  minveclem6  23494  ovolunnul  23558  voliunlem3  23610  ovolioo  23626  itg2splitlem  23806  itg2split  23807  itgrevallem1  23852  itgsplitioo  23895  ditgsplit  23916  dvnadd  23983  dvlipcn  24048  ply1divex  24187  dvntaylp  24416  ulmshft  24435  abelthlem6  24481  cosmpi  24532  sinppi  24533  sinhalfpip  24536  logrnaddcl  24612  affineequiv  24844  chordthmlem3  24852  atanlogaddlem  24931  atanlogsublem  24933  leibpi  24960  scvxcvx  25003  dmgmn0  25043  lgamgulmlem2  25047  lgambdd  25054  logexprlim  25241  2sqblem  25447  dchrvmasum2if  25477  dchrvmasumlem  25503  axcontlem8  26142  crctcshlem4  27005  eupth2lem3lem6  27511  ipidsq  28021  minvecolem6  28194  normpyc  28459  pjspansn  28892  lnfnmuli  29359  hstoh  29547  archirngz  30190  indsumin  30531  esumpfinvallem  30583  signsvtp  31111  signlem0  31115  fsum2dsub  31136  cvxpconn  31672  cvxsconn  31673  elmrsubrn  31865  faclim2  32079  fwddifn0  32715  fwddifnp1  32716  dnizeq0  32904  knoppndvlem6  32947  bj-bary1lem  33594  poimirlem1  33834  poimirlem5  33838  poimirlem6  33839  poimirlem7  33840  poimirlem11  33844  poimirlem12  33845  poimirlem17  33850  poimirlem20  33853  poimirlem22  33855  poimirlem24  33857  poimirlem25  33858  poimirlem29  33862  poimirlem31  33864  mblfinlem2  33871  mbfposadd  33880  itg2addnc  33887  itgaddnclem2  33892  ftc1anclem5  33912  ftc1anclem8  33915  areacirc  33928  pell1qrgaplem  38115  jm2.19lem3  38235  jm2.25  38243  relexpaddss  38685  int-add01d  39161  binomcxplemnn0  39222  fperiodmullem  40156  xralrple3  40228  sumnnodd  40500  fprodaddrecnncnvlem  40761  ioodvbdlimc1lem2  40785  volioc  40825  volico  40837  stoweidlem11  40865  stoweidlem26  40880  stirlinglem12  40939  fourierdlem4  40965  fourierdlem42  41003  fourierdlem60  41020  fourierdlem61  41021  fourierdlem92  41052  fourierdlem107  41067  fouriersw  41085  etransclem24  41112  etransclem35  41123  hoidmvlelem2  41450  hspmbllem1  41480  sharhght  41694  deccarry  42055  altgsumbcALT  42800
  Copyright terms: Public domain W3C validator