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

Theorem mul01d 9564
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 9544 . 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 1364    e. wcel 1761  (class class class)co 6090   CCcc 9276   0cc0 9278    x. cmul 9283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-po 4637  df-so 4638  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-er 7097  df-en 7307  df-dom 7308  df-sdom 7309  df-pnf 9416  df-mnf 9417  df-ltxr 9419
This theorem is referenced by:  mulge0  9853  mul0or  9972  diveq0  10000  div0  10018  lemul1a  10179  un0mulcl  10610  rexmul  11230  modid  11728  expmul  11905  sqlecan  11968  discr  11997  hashf1lem2  12205  hashf1  12206  fsummulc2  13247  geolim  13326  geomulcvg  13332  0dvds  13549  smumullem  13684  bezoutlem1  13718  mulgcddvds  13786  prmdiv  13856  pcaddlem  13946  qexpz  13959  prmreclem4  13976  prmreclem5  13977  mulgnn0ass  15649  odadd2  16324  isabvd  16885  nn0srg  17781  rge0srg  17782  nmolb2d  20197  nmoleub  20210  reparphti  20469  pcorevlem  20498  itg1val2  21062  i1fmullem  21072  itg1addlem4  21077  itg10a  21088  itg1ge0a  21089  itg2const  21118  itg2monolem1  21128  itg0  21157  itgz  21158  iblmulc2  21208  itgmulc2lem1  21209  bddmulibl  21216  dvcnp2  21294  dvcobr  21320  dvlip  21365  dvlipcn  21366  c1lip1  21369  dvlt0  21377  plymullem1  21625  coefv0  21658  coemullem  21660  coemulhi  21664  dgrmulc  21681  dgrcolem2  21684  dvply1  21693  plydivlem3  21704  elqaalem2  21729  elqaalem3  21730  tayl0  21770  dvtaylp  21778  radcnv0  21824  dvradcnv  21829  pserdvlem2  21836  abelthlem2  21840  pilem2  21860  sinmpi  21892  cosmpi  21893  sinppi  21894  cosppi  21895  tanregt0  21938  argregt0  22002  argrege0  22003  argimgt0  22004  logtayl  22048  mulcxplem  22072  mulcxp  22073  cxpmul2  22077  pythag  22156  quad2  22177  dcubic  22184  atans2  22269  mumul  22462  logexprlim  22507  dchrsum2  22550  sumdchr2  22552  lgsdilem  22604  lgsdirnn0  22621  lgsdinn0  22622  lgsquad3  22643  rpvmasumlem  22679  dchrisumlem1  22681  dchrvmasumiflem2  22694  rpvmasum2  22704  dchrisum0re  22705  pntrlog2bndlem4  22772  pntlemf  22797  pntleml  22803  ostth2lem2  22826  ostth3  22830  colinearalg  23075  gxnn0mul  23683  nmlnoubi  24115  ipasslem2  24151  cdj3lem1  25757  mul2lt0bi  25961  xrge0iifhom  26287  sgnmul  26839  signsplypnf  26865  signswch  26876  signlem0  26902  zetacvg  26915  lgamgulmlem2  26930  fprodeq0  27399  0risefac  27454  ovoliunnfl  28342  voliunnfl  28344  itg2addnclem  28352  iblmulc2nc  28366  itgmulc2nclem1  28367  areacirc  28398  geomcau  28564  bfp  28632  irrapxlem1  29072  pell1qr1  29121  pell1qrgaplem  29123  rmxy0  29173  jm2.18  29246  mpaaeu  29416  stoweidlem26  29730  stoweidlem37  29741  stirlinglem7  29784  sharhght  29810  altgsumbc  30650
  Copyright terms: Public domain W3C validator