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

Theorem mul01d 9782
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 9762 . 2  |-  ( A  e.  CC  ->  ( A  x.  0 )  =  0 )
31, 2syl 16 1  |-  ( ph  ->  ( A  x.  0 )  =  0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804  (class class class)co 6281   CCcc 9493   0cc0 9495    x. cmul 9500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-po 4790  df-so 4791  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-ltxr 9636
This theorem is referenced by:  mulge0  10077  mul0or  10196  diveq0  10224  div0  10242  lemul1a  10403  un0mulcl  10837  rexmul  11474  modid  12002  expmul  12193  sqlecan  12256  discr  12285  hashf1lem2  12487  hashf1  12488  fsummulc2  13581  geolim  13661  geomulcvg  13667  fprodeq0  13761  0dvds  13986  smumullem  14124  bezoutlem1  14158  mulgcddvds  14227  prmdiv  14297  pcaddlem  14389  qexpz  14402  prmreclem4  14419  prmreclem5  14420  mulgnn0ass  16150  odadd2  16834  isabvd  17448  nn0srg  18465  rge0srg  18466  nmolb2d  21203  nmoleub  21216  reparphti  21475  pcorevlem  21504  itg1val2  22069  i1fmullem  22079  itg1addlem4  22084  itg10a  22095  itg1ge0a  22096  itg2const  22125  itg2monolem1  22135  itg0  22164  itgz  22165  iblmulc2  22215  itgmulc2lem1  22216  bddmulibl  22223  dvcnp2  22301  dvcobr  22327  dvlip  22372  dvlipcn  22373  c1lip1  22376  dvlt0  22384  plymullem1  22589  coefv0  22623  coemullem  22625  coemulhi  22629  dgrmulc  22646  dgrcolem2  22649  dvply1  22658  plydivlem3  22669  elqaalem2  22694  elqaalem3  22695  tayl0  22735  dvtaylp  22743  radcnv0  22789  dvradcnv  22794  pserdvlem2  22801  abelthlem2  22805  pilem2  22825  sinmpi  22858  cosmpi  22859  sinppi  22860  cosppi  22861  tanregt0  22904  efsubm  22916  argregt0  22973  argrege0  22974  argimgt0  22975  logtayl  23019  mulcxplem  23043  mulcxp  23044  cxpmul2  23048  pythag  23127  quad2  23148  dcubic  23155  atans2  23240  mumul  23433  logexprlim  23478  dchrsum2  23521  sumdchr2  23523  lgsdilem  23575  lgsdirnn0  23592  lgsdinn0  23593  lgsquad3  23614  rpvmasumlem  23650  dchrisumlem1  23652  dchrvmasumiflem2  23665  rpvmasum2  23675  dchrisum0re  23676  pntrlog2bndlem4  23743  pntlemf  23768  pntleml  23774  ostth2lem2  23797  ostth3  23801  colinearalg  24191  gxnn0mul  25257  nmlnoubi  25689  ipasslem2  25725  cdj3lem1  27331  mul2lt0bi  27547  2sqmod  27614  xrge0iifhom  27897  sgnmul  28459  signsplypnf  28485  signswch  28496  signlem0  28522  zetacvg  28535  lgamgulmlem2  28550  0risefac  29136  ovoliunnfl  30032  voliunnfl  30034  itg2addnclem  30042  iblmulc2nc  30056  itgmulc2nclem1  30057  areacirc  30088  geomcau  30228  bfp  30296  irrapxlem1  30734  pell1qr1  30783  pell1qrgaplem  30785  rmxy0  30835  jm2.18  30906  mpaaeu  31075  lcmgcd  31189  stoweidlem26  31762  stoweidlem37  31773  stirlinglem7  31816  dirkercncflem2  31840  fourierdlem103  31946  fourierdlem104  31947  sqwvfoura  31965  sqwvfourb  31966  etransclem15  31986  etransclem24  31995  etransclem25  31996  etransclem32  32003  etransclem35  32006  etransclem48  32019  sharhght  32036  altgsumbcALT  32810
  Copyright terms: Public domain W3C validator