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

Theorem mul01d 9833
Description: Multiplication by  0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
mul01d  |-  ( ph  ->  ( A  x.  0 )  =  0 )

Proof of Theorem mul01d
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 mul01 9813 . 2  |-  ( A  e.  CC  ->  ( A  x.  0 )  =  0 )
31, 2syl 17 1  |-  ( ph  ->  ( A  x.  0 )  =  0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1868  (class class class)co 6302   CCcc 9538   0cc0 9540    x. cmul 9545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-po 4771  df-so 4772  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-ov 6305  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-pnf 9678  df-mnf 9679  df-ltxr 9681
This theorem is referenced by:  mulge0  10133  mul0or  10253  diveq0  10281  div0  10299  lemul1a  10460  un0mulcl  10905  mul2lt0bi  11403  rexmul  11558  modid  12121  expmul  12317  sqlecan  12381  discr  12409  hashf1lem2  12617  hashf1  12618  fsummulc2  13833  geolim  13914  geomulcvg  13920  fprodeq0  14017  0risefac  14079  0dvds  14311  smumullem  14454  bezoutlem1  14491  lcmgcd  14560  mulgcddvds  14649  prmdiv  14721  pcaddlem  14821  qexpz  14834  prmreclem4  14851  prmreclem5  14852  mulgnn0ass  16775  odadd2  17475  isabvd  18036  nn0srg  19024  rge0srg  19025  nmolb2d  21710  nmoleub  21723  nmoleubOLD  21739  reparphti  22015  pcorevlem  22044  itg1val2  22629  i1fmullem  22639  itg1addlem4  22644  itg10a  22655  itg1ge0a  22656  itg2const  22685  itg2monolem1  22695  itg0  22724  itgz  22725  iblmulc2  22775  itgmulc2lem1  22776  bddmulibl  22783  dvcnp2  22861  dvcobr  22887  dvlip  22932  dvlipcn  22933  c1lip1  22936  dvlt0  22944  plymullem1  23155  coefv0  23189  coemullem  23191  coemulhi  23195  dgrmulc  23212  dgrcolem2  23215  dvply1  23224  plydivlem3  23235  elqaalem2  23260  elqaalem3  23261  elqaalem2OLD  23263  elqaalem3OLD  23264  tayl0  23304  dvtaylp  23312  radcnv0  23358  dvradcnv  23363  pserdvlem2  23370  abelthlem2  23374  pilem2  23394  pilem2OLD  23395  sinmpi  23429  cosmpi  23430  sinppi  23431  cosppi  23432  tanregt0  23475  efsubm  23487  argregt0  23546  argrege0  23547  argimgt0  23548  logtayl  23592  mulcxplem  23616  mulcxp  23617  cxpmul2  23621  pythag  23733  quad2  23752  dcubic  23759  atans2  23844  zetacvg  23927  lgamgulmlem2  23942  mumul  24095  logexprlim  24140  dchrsum2  24183  sumdchr2  24185  lgsdilem  24237  lgsdirnn0  24254  lgsdinn0  24255  lgsquad3  24276  rpvmasumlem  24312  dchrisumlem1  24314  dchrvmasumiflem2  24327  rpvmasum2  24337  dchrisum0re  24338  pntrlog2bndlem4  24405  pntlemf  24430  pntleml  24436  ostth2lem2  24459  ostth3  24463  colinearalg  24927  gxnn0mul  25991  nmlnoubi  26423  ipasslem2  26459  cdj3lem1  28073  2sqmod  28404  xrge0iifhom  28739  sgnmul  29409  signsplypnf  29435  signswch  29446  signlem0  29472  ovoliunnfl  31896  voliunnfl  31898  itg2addnclem  31907  iblmulc2nc  31921  itgmulc2nclem1  31922  areacirc  31951  geomcau  32002  bfp  32070  irrapxlem1  35586  pell1qr1  35637  pell1qrgaplem  35639  rmxy0  35691  jm2.18  35763  mpaaeu  35936  relexpmulg  36162  binomcxplemnotnn0  36563  stoweidlem26  37706  stoweidlem37  37718  stirlinglem7  37762  dirkercncflem2  37786  fourierdlem103  37893  fourierdlem104  37894  sqwvfoura  37912  sqwvfourb  37913  etransclem15  37934  etransclem24  37943  etransclem25  37944  etransclem32  37951  etransclem35  37954  etransclem48OLD  37967  etransclem48  37968  sharhght  38187  altgsumbcALT  39408  dig0  39691
  Copyright terms: Public domain W3C validator