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

Theorem mul01d 9568
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 9548 . 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 1369    e. wcel 1756  (class class class)co 6091   CCcc 9280   0cc0 9282    x. cmul 9287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-addrcl 9343  ax-mulcl 9344  ax-mulrcl 9345  ax-mulcom 9346  ax-addass 9347  ax-mulass 9348  ax-distr 9349  ax-i2m1 9350  ax-1ne0 9351  ax-1rid 9352  ax-rnegex 9353  ax-rrecex 9354  ax-cnre 9355  ax-pre-lttri 9356  ax-pre-lttrn 9357  ax-pre-ltadd 9358
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-po 4641  df-so 4642  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ov 6094  df-er 7101  df-en 7311  df-dom 7312  df-sdom 7313  df-pnf 9420  df-mnf 9421  df-ltxr 9423
This theorem is referenced by:  mulge0  9857  mul0or  9976  diveq0  10004  div0  10022  lemul1a  10183  un0mulcl  10614  rexmul  11234  modid  11732  expmul  11909  sqlecan  11972  discr  12001  hashf1lem2  12209  hashf1  12210  fsummulc2  13251  geolim  13330  geomulcvg  13336  0dvds  13553  smumullem  13688  bezoutlem1  13722  mulgcddvds  13790  prmdiv  13860  pcaddlem  13950  qexpz  13963  prmreclem4  13980  prmreclem5  13981  mulgnn0ass  15656  odadd2  16331  isabvd  16905  nn0srg  17881  rge0srg  17882  nmolb2d  20297  nmoleub  20310  reparphti  20569  pcorevlem  20598  itg1val2  21162  i1fmullem  21172  itg1addlem4  21177  itg10a  21188  itg1ge0a  21189  itg2const  21218  itg2monolem1  21228  itg0  21257  itgz  21258  iblmulc2  21308  itgmulc2lem1  21309  bddmulibl  21316  dvcnp2  21394  dvcobr  21420  dvlip  21465  dvlipcn  21466  c1lip1  21469  dvlt0  21477  plymullem1  21682  coefv0  21715  coemullem  21717  coemulhi  21721  dgrmulc  21738  dgrcolem2  21741  dvply1  21750  plydivlem3  21761  elqaalem2  21786  elqaalem3  21787  tayl0  21827  dvtaylp  21835  radcnv0  21881  dvradcnv  21886  pserdvlem2  21893  abelthlem2  21897  pilem2  21917  sinmpi  21949  cosmpi  21950  sinppi  21951  cosppi  21952  tanregt0  21995  argregt0  22059  argrege0  22060  argimgt0  22061  logtayl  22105  mulcxplem  22129  mulcxp  22130  cxpmul2  22134  pythag  22213  quad2  22234  dcubic  22241  atans2  22326  mumul  22519  logexprlim  22564  dchrsum2  22607  sumdchr2  22609  lgsdilem  22661  lgsdirnn0  22678  lgsdinn0  22679  lgsquad3  22700  rpvmasumlem  22736  dchrisumlem1  22738  dchrvmasumiflem2  22751  rpvmasum2  22761  dchrisum0re  22762  pntrlog2bndlem4  22829  pntlemf  22854  pntleml  22860  ostth2lem2  22883  ostth3  22887  colinearalg  23156  gxnn0mul  23764  nmlnoubi  24196  ipasslem2  24232  cdj3lem1  25838  mul2lt0bi  26042  xrge0iifhom  26367  sgnmul  26925  signsplypnf  26951  signswch  26962  signlem0  26988  zetacvg  27001  lgamgulmlem2  27016  fprodeq0  27486  0risefac  27541  ovoliunnfl  28433  voliunnfl  28435  itg2addnclem  28443  iblmulc2nc  28457  itgmulc2nclem1  28458  areacirc  28489  geomcau  28655  bfp  28723  irrapxlem1  29163  pell1qr1  29212  pell1qrgaplem  29214  rmxy0  29264  jm2.18  29337  mpaaeu  29507  stoweidlem26  29821  stoweidlem37  29832  stirlinglem7  29875  sharhght  29901  altgsumbcALT  30750
  Copyright terms: Public domain W3C validator