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

Theorem mul01d 10087
Description: Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
mul01d (𝜑 → (𝐴 · 0) = 0)

Proof of Theorem mul01d
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 mul01 10067 . 2 (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
31, 2syl 17 1 (𝜑 → (𝐴 · 0) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  (class class class)co 6527  cc 9791  0cc0 9793   · cmul 9798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-ltxr 9936
This theorem is referenced by:  mulge0  10398  mul0or  10519  diveq0  10547  div0  10567  lemul1a  10729  un0mulcl  11177  mul2lt0bi  11771  rexmul  11933  modid  12515  addmodlteq  12565  expmul  12725  sqlecan  12791  discr  12821  hashf1lem2  13052  hashf1  13053  fsummulc2  14307  geolim  14389  geomulcvg  14395  fprodeq0  14493  0risefac  14557  0dvds  14789  smumullem  15001  bezoutlem1  15043  lcmgcd  15107  mulgcddvds  15156  cncongr2  15169  prmdiv  15277  pcaddlem  15379  qexpz  15392  prmreclem4  15410  prmreclem5  15411  mulgnn0ass  17350  odadd2  18024  isabvd  18592  nn0srg  19584  rge0srg  19585  nmolb2d  22280  nmoleub  22293  reparphti  22553  pcorevlem  22582  itg1val2  23202  i1fmullem  23212  itg1addlem4  23217  itg10a  23228  itg1ge0a  23229  itg2const  23258  itg2monolem1  23268  itg0  23297  itgz  23298  iblmulc2  23348  itgmulc2lem1  23349  bddmulibl  23356  dvcnp2  23434  dvcobr  23460  dvlip  23505  dvlipcn  23506  c1lip1  23509  dvlt0  23517  plymullem1  23719  coefv0  23753  coemullem  23755  coemulhi  23759  dgrmulc  23776  dgrcolem2  23779  dvply1  23788  plydivlem3  23799  elqaalem2  23824  elqaalem3  23825  tayl0  23865  dvtaylp  23873  radcnv0  23919  dvradcnv  23924  pserdvlem2  23931  abelthlem2  23935  pilem2  23955  sinmpi  23988  cosmpi  23989  sinppi  23990  cosppi  23991  tanregt0  24034  efsubm  24046  argregt0  24105  argrege0  24106  argimgt0  24107  logtayl  24151  mulcxplem  24175  mulcxp  24176  cxpmul2  24180  pythag  24292  quad2  24311  dcubic  24318  atans2  24403  zetacvg  24486  lgamgulmlem2  24501  mumul  24652  logexprlim  24695  dchrsum2  24738  sumdchr2  24740  lgsdilem  24794  lgsdirnn0  24814  lgsdinn0  24815  lgsquad3  24857  rpvmasumlem  24921  dchrisumlem1  24923  dchrvmasumiflem2  24936  rpvmasum2  24946  dchrisum0re  24947  pntrlog2bndlem4  25014  pntlemf  25039  pntleml  25045  ostth2lem2  25068  ostth3  25072  colinearalg  25536  nmlnoubi  26869  ipasslem2  26905  cdj3lem1  28511  2sqmod  28813  xrge0iifhom  29145  sgnmul  29765  signsplypnf  29787  signswch  29798  signlem0  29824  knoppndvlem6  31512  knoppndvlem8  31514  knoppndvlem13  31519  ovoliunnfl  32445  voliunnfl  32447  itg2addnclem  32455  iblmulc2nc  32469  itgmulc2nclem1  32470  areacirc  32499  geomcau  32549  bfp  32617  irrapxlem1  36228  pell1qr1  36277  pell1qrgaplem  36279  rmxy0  36330  jm2.18  36397  mpaaeu  36563  relexpmulg  36845  binomcxplemnotnn0  37401  xralrple2  38335  stoweidlem26  38743  stoweidlem37  38754  stirlinglem7  38797  dirkercncflem2  38821  fourierdlem103  38926  fourierdlem104  38927  sqwvfoura  38945  sqwvfourb  38946  etransclem15  38966  etransclem24  38975  etransclem25  38976  etransclem32  38983  etransclem35  38986  etransclem48  38999  hoidmvlelem1  39309  hoidmvlelem2  39310  hoidmvlelem3  39311  sharhght  39527  pwdif  39864  altgsumbcALT  41946  dig0  42220
  Copyright terms: Public domain W3C validator