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

Theorem mul01d 9254
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 9234 . 2  |-  ( A  e.  CC  ->  ( A  x.  0 )  =  0 )
31, 2syl 16 1  |-  ( ph  ->  ( A  x.  0 )  =  0 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725  (class class class)co 6072   CCcc 8977   0cc0 8979    x. cmul 8984
This theorem is referenced by:  mulge0  9534  mul0or  9651  diveq0  9677  div0  9695  lemul1a  9853  un0mulcl  10243  rexmul  10839  modid  11258  expmul  11413  sqlecan  11475  discr  11504  hashf1lem2  11693  hashf1  11694  fsummulc2  12555  geolim  12635  geomulcvg  12641  0dvds  12858  smumullem  12992  bezoutlem1  13026  mulgcddvds  13092  prmdiv  13162  pcaddlem  13245  qexpz  13258  prmreclem4  13275  prmreclem5  13276  mulgnn0ass  14907  odadd2  15452  isabvd  15896  nmolb2d  18740  nmoleub  18753  reparphti  19010  pcorevlem  19039  itg1val2  19564  i1fmullem  19574  itg1addlem4  19579  itg10a  19590  itg1ge0a  19591  itg2const  19620  itg2monolem1  19630  itg0  19659  itgz  19660  iblmulc2  19710  itgmulc2lem1  19711  bddmulibl  19718  dvcnp2  19794  dvcobr  19820  dvlip  19865  dvlipcn  19866  c1lip1  19869  dvlt0  19877  plymullem1  20121  coefv0  20154  coemullem  20156  coemulhi  20160  dgrmulc  20177  dgrcolem2  20180  dvply1  20189  plydivlem3  20200  elqaalem2  20225  elqaalem3  20226  tayl0  20266  dvtaylp  20274  radcnv0  20320  dvradcnv  20325  pserdvlem2  20332  abelthlem2  20336  pilem2  20356  sinmpi  20383  cosmpi  20384  sinppi  20385  cosppi  20386  tanregt0  20429  argregt0  20493  argrege0  20494  argimgt0  20495  logtayl  20539  mulcxplem  20563  mulcxp  20564  cxpmul2  20568  pythag  20647  quad2  20667  dcubic  20674  atans2  20759  mumul  20952  logexprlim  20997  dchrsum2  21040  sumdchr2  21042  lgsdilem  21094  lgsdirnn0  21111  lgsdinn0  21112  lgsquad3  21133  rpvmasumlem  21169  dchrisumlem1  21171  dchrvmasumiflem2  21184  rpvmasum2  21194  dchrisum0re  21195  pntrlog2bndlem4  21262  pntlemf  21287  pntleml  21293  ostth2lem2  21316  ostth3  21320  gxnn0mul  21853  nmlnoubi  22285  ipasslem2  22321  cdj3lem1  23925  xrge0iifhom  24311  zetacvg  24787  lgamgulmlem2  24802  fprodeq0  25288  0risefac  25343  colinearalg  25797  ovoliunnfl  26194  voliunnfl  26196  itg2addnclem  26202  iblmulc2nc  26216  itgmulc2nclem1  26217  areacirc  26234  geomcau  26402  bfp  26470  irrapxlem1  26822  pell1qr1  26871  pell1qrgaplem  26873  rmxy0  26923  jm2.18  26996  mpaaeu  27270  stoweidlem26  27689  stoweidlem37  27700  stirlinglem7  27743  sharhght  27769
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692  ax-resscn 9036  ax-1cn 9037  ax-icn 9038  ax-addcl 9039  ax-addrcl 9040  ax-mulcl 9041  ax-mulrcl 9042  ax-mulcom 9043  ax-addass 9044  ax-mulass 9045  ax-distr 9046  ax-i2m1 9047  ax-1ne0 9048  ax-1rid 9049  ax-rnegex 9050  ax-rrecex 9051  ax-cnre 9052  ax-pre-lttri 9053  ax-pre-lttrn 9054  ax-pre-ltadd 9055
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-po 4495  df-so 4496  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-er 6896  df-en 7101  df-dom 7102  df-sdom 7103  df-pnf 9111  df-mnf 9112  df-ltxr 9114
  Copyright terms: Public domain W3C validator