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

Theorem addid1d 11356
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 11336 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  (class class class)co 7358  cc 11050  0cc0 11052   + caddc 11055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-po 5546  df-so 5547  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-ltxr 11195
This theorem is referenced by:  ltaddneg  11371  subsub2  11430  negsub  11450  ltaddpos  11646  addge01  11666  add20  11668  nnge1  12182  nnnn0addcl  12444  un0addcl  12447  uzaddcl  12830  xaddid1  13161  fzosubel3  13634  expadd  14011  faclbnd4lem4  14197  faclbnd6  14200  hashgadd  14278  ccatrid  14476  pfxmpt  14567  pfxfv  14571  pfxswrd  14595  pfxccatin12lem1  14617  pfxccatin12lem2  14620  swrdccat3blem  14628  cshweqrep  14710  relexpaddg  14939  reim0b  15005  rereb  15006  immul2  15023  max0add  15196  iseraltlem2  15568  fsumsplit  15627  sumsplit  15654  binomfallfaclem2  15924  pwp1fsum  16274  bitsinv1lem  16322  sadadd2lem2  16331  sadcaddlem  16338  bezoutlem1  16421  pcadd  16762  pcadd2  16763  pcmpt  16765  vdwapun  16847  vdwlem1  16854  mulgnn0dir  18907  psgnunilem2  19278  sylow1lem1  19381  efginvrel2  19510  efgredleme  19526  efgcpbllemb  19538  frgpnabllem1  19652  regsumfsum  20868  regsumsupp  21029  mplcoe5  21444  xrsxmet  24175  reparphti  24363  cphpyth  24583  minveclem6  24801  ovolunnul  24867  voliunlem3  24919  ovolioo  24935  itg2splitlem  25116  itg2split  25117  itgrevallem1  25162  itgsplitioo  25205  ditgsplit  25228  dvnadd  25296  dvlipcn  25361  ply1divex  25504  dvntaylp  25733  ulmshft  25752  abelthlem6  25798  cosmpi  25848  sinppi  25849  sinhalfpip  25852  logrnaddcl  25933  affineequiv  26176  chordthmlem3  26187  atanlogaddlem  26266  atanlogsublem  26268  leibpi  26295  scvxcvx  26338  dmgmn0  26378  lgamgulmlem2  26382  lgambdd  26389  logexprlim  26576  2sqblem  26782  2sq2  26784  2sqnn  26790  dchrvmasum2if  26848  dchrvmasumlem  26874  axcontlem8  27923  elntg2  27937  crctcshlem4  28768  eupth2lem3lem6  29180  ipidsq  29655  minvecolem6  29827  normpyc  30091  pjspansn  30522  lnfnmuli  30989  hstoh  31177  archirngz  32028  indsumin  32624  esumpfinvallem  32676  signsvtp  33198  signlem0  33202  fsum2dsub  33223  cvxpconn  33839  cvxsconn  33840  elmrsubrn  34117  faclim2  34324  fwddifn0  34752  fwddifnp1  34753  dnizeq0  34941  knoppndvlem6  34983  bj-bary1lem  35784  poimirlem1  36082  poimirlem5  36086  poimirlem6  36087  poimirlem7  36088  poimirlem11  36092  poimirlem12  36093  poimirlem17  36098  poimirlem20  36101  poimirlem22  36103  poimirlem24  36105  poimirlem25  36106  poimirlem29  36110  poimirlem31  36112  mblfinlem2  36119  mbfposadd  36128  itg2addnc  36135  itgaddnclem2  36140  ftc1anclem5  36158  ftc1anclem8  36161  areacirc  36174  lcmineqlem4  40492  lcmineqlem18  40506  aks4d1p1p7  40534  aks4d1p3  40538  sticksstones10  40566  sticksstones12a  40568  metakunt29  40608  metakunt30  40609  3cubeslem2  41011  3cubeslem3r  41013  pell1qrgaplem  41199  jm2.19lem3  41318  jm2.25  41326  relexpaddss  41997  int-add01d  42464  binomcxplemnn0  42636  fperiodmullem  43544  xralrple3  43615  sumnnodd  43878  fprodaddrecnncnvlem  44157  ioodvbdlimc1lem2  44180  volioc  44220  volico  44231  stoweidlem11  44259  stoweidlem26  44274  stirlinglem12  44333  fourierdlem4  44359  fourierdlem42  44397  fourierdlem60  44414  fourierdlem61  44415  fourierdlem92  44446  fourierdlem107  44461  fouriersw  44479  etransclem24  44506  etransclem35  44517  hoidmvlelem2  44844  hspmbllem1  44874  sharhght  45113  deccarry  45550  nn0mnd  46120  altgsumbcALT  46436  itcovalpclem1  46763  eenglngeehlnmlem2  46831  line2y  46848  itschlc0xyqsol1  46859  itschlc0xyqsol  46860  2itscp  46874
  Copyright terms: Public domain W3C validator