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

Theorem mul02d 9253
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
mul02d  |-  ( ph  ->  ( 0  x.  A
)  =  0 )

Proof of Theorem mul02d
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 mul02 9233 . 2  |-  ( A  e.  CC  ->  (
0  x.  A )  =  0 )
31, 2syl 16 1  |-  ( ph  ->  ( 0  x.  A
)  =  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:  mulneg1  9459  mulge0  9534  mul0or  9651  prodgt0  9844  un0mulcl  10243  lincmb01cmp  11027  iccf1o  11028  discr1  11503  discr  11504  hashxplem  11684  remul2  11923  immul2  11930  binomlem  12596  geomulcvg  12641  efne0  12686  dvds0  12853  smumullem  12992  mulgcd  13034  qnumgt0  13130  pcexp  13221  vdwapun  13330  vdwlem1  13337  mulgnn0ass  14907  odmulg  15180  torsubg  15457  isabvd  15896  prmirredlem  16761  nmo0  18757  nmoeq0  18758  blcvx  18817  reparphti  19010  pcorevlem  19039  ipcau2  19179  itg1addlem4  19579  itg1addlem5  19580  itg1mulc  19584  itg2mulc  19627  dvcmul  19818  dvmptcmul  19838  dvexp3  19850  dvef  19852  dveq0  19872  dv11cn  19873  ply1termlem  20110  plyeq0lem  20117  plypf1  20119  plyaddlem1  20120  plymullem1  20121  coeeulem  20131  coeidlem  20144  coeid3  20147  coemullem  20156  coemulhi  20160  coemulc  20161  dgrco  20181  vieta1lem2  20216  elqaalem2  20225  aalioulem3  20239  taylthlem2  20278  abelthlem6  20340  pilem2  20356  sinhalfpip  20388  sinhalfpim  20389  coshalfpip  20390  coshalfpim  20391  logtayl  20539  mulcxp  20564  cxpmul2  20568  cxpeq  20629  chordthmlem5  20665  cubic  20677  atans2  20759  atantayl2  20766  leibpi  20770  efrlim  20796  scvxcvx  20812  amgm  20817  ftalem5  20847  basellem2  20852  mumul  20952  muinv  20966  dchrn0  21022  dchrinvcl  21025  lgsdirnn0  21111  lgsdinn0  21112  lgsquad2lem2  21131  rpvmasumlem  21169  dchrisum0flblem1  21190  rpvmasum2  21194  ostth2lem2  21316  nvz0  22145  ipasslem1  22320  hi01  22586  xrge0iifhom  24311  indsum  24408  subfacp1lem6  24859  cvxpcon  24917  cvxscon  24918  ntrivcvgfvn0  25216  fprodeq0  25288  0fallfac  25342  binomfallfaclem2  25345  brbtwn2  25792  axsegconlem1  25804  axpaschlem  25827  axcontlem7  25857  axcontlem8  25858  pell1234qrne0  26853  bezoutr1  26988  jm2.19lem3  26999  jm2.25  27007  flcidc  27294  dvconstbi  27466  itgsinexplem1  27662  sigarcol  27768  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