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

Theorem mul01d 10832
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 10812 . 2 (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
31, 2syl 17 1 (𝜑 → (𝐴 · 0) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112  (class class class)co 7139  cc 10528  0cc0 10530   · cmul 10535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-po 5442  df-so 5443  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10670  df-mnf 10671  df-ltxr 10673
This theorem is referenced by:  mulge0  11151  mul0or  11273  diveq0  11301  div0  11321  lemul1a  11487  un0mulcl  11923  mul2lt0bi  12487  rexmul  12656  modid  13263  addmodlteq  13313  expmul  13474  sqlecan  13571  discr  13601  hashf1lem2  13814  hashf1  13815  fsummulc2  15134  pwdif  15218  geolim  15221  geomulcvg  15227  fprodeq0  15324  0risefac  15387  0dvds  15625  smumullem  15834  bezoutlem1  15880  lcmgcd  15944  mulgcddvds  15992  cncongr2  16005  prmdiv  16115  pcaddlem  16217  qexpz  16230  prmreclem4  16248  prmreclem5  16249  mulgnn0ass  18258  odadd2  18965  isabvd  19587  nn0srg  20164  rge0srg  20165  nmolb2d  23327  nmoleub  23340  reparphti  23605  pcorevlem  23634  itg1val2  24291  i1fmullem  24301  itg1addlem4  24306  itg10a  24317  itg1ge0a  24318  itg2const  24347  itg2monolem1  24357  itg0  24386  itgz  24387  iblmulc2  24437  itgmulc2lem1  24438  bddmulibl  24445  dvcnp2  24526  dvcobr  24552  dvlip  24599  dvlipcn  24600  c1lip1  24603  dvlt0  24611  plymullem1  24814  coefv0  24848  coemullem  24850  coemulhi  24854  dgrmulc  24871  dgrcolem2  24874  dvply1  24883  plydivlem3  24894  elqaalem2  24919  elqaalem3  24920  tayl0  24960  dvtaylp  24968  radcnv0  25014  dvradcnv  25019  pserdvlem2  25026  abelthlem2  25030  pilem2  25050  sinmpi  25083  cosmpi  25084  sinppi  25085  cosppi  25086  tanregt0  25134  efsubm  25146  argregt0  25204  argrege0  25205  argimgt0  25206  logtayl  25254  mulcxplem  25278  mulcxp  25279  cxpmul2  25283  pythag  25406  quad2  25428  dcubic  25435  atans2  25520  zetacvg  25603  lgamgulmlem2  25618  mumul  25769  logexprlim  25812  dchrsum2  25855  sumdchr2  25857  lgsdilem  25911  lgsdirnn0  25931  lgsdinn0  25932  lgsquad3  25974  2sqmod  26023  rpvmasumlem  26074  dchrisumlem1  26076  dchrvmasumiflem2  26089  rpvmasum2  26099  dchrisum0re  26100  pntrlog2bndlem4  26167  pntlemf  26192  pntleml  26198  ostth2lem2  26221  ostth3  26225  colinearalg  26707  nmlnoubi  28582  ipasslem2  28618  cdj3lem1  30220  xrge0iifhom  31288  sgnmul  31908  signsplypnf  31928  signswch  31939  signlem0  31965  itgexpif  31985  circlemeth  32019  knoppndvlem6  33964  knoppndvlem8  33966  knoppndvlem13  33971  ovoliunnfl  35092  voliunnfl  35094  itg2addnclem  35101  iblmulc2nc  35115  itgmulc2nclem1  35116  areacirc  35143  geomcau  35190  bfp  35255  lcmineqlem10  39319  lcmineqlem12  39321  irrapxlem1  39750  pell1qr1  39799  pell1qrgaplem  39801  rmxy0  39851  jm2.18  39916  mpaaeu  40081  relexpmulg  40398  binomcxplemnotnn0  41047  xralrple2  41973  stoweidlem26  42655  stoweidlem37  42666  stirlinglem7  42709  dirkercncflem2  42733  fourierdlem103  42838  fourierdlem104  42839  sqwvfoura  42857  sqwvfourb  42858  etransclem15  42878  etransclem24  42887  etransclem25  42888  etransclem32  42895  etransclem35  42898  etransclem48  42911  hoidmvlelem1  43221  hoidmvlelem2  43222  hoidmvlelem3  43223  sharhght  43466  altgsumbcALT  44742  dig0  45007  itcovalpclem1  45071  line2ylem  45152  line2xlem  45154  2itscp  45182
  Copyright terms: Public domain W3C validator