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

Theorem mul02d 9005
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 8985 . 2  |-  ( A  e.  CC  ->  (
0  x.  A )  =  0 )
31, 2syl 17 1  |-  ( ph  ->  ( 0  x.  A
)  =  0 )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1624    e. wcel 1685  (class class class)co 5819   CCcc 8730   0cc0 8732    x. cmul 8737
This theorem is referenced by:  mulneg1  9211  mulge0  9286  mul0or  9403  prodgt0  9596  un0mulcl  9993  lincmb01cmp  10771  iccf1o  10772  discr1  11231  discr  11232  hashxplem  11379  remul2  11609  immul2  11616  binomlem  12281  geomulcvg  12326  efne0  12371  dvds0  12538  smumullem  12677  mulgcd  12719  qnumgt0  12815  pcexp  12906  vdwapun  13015  vdwlem1  13022  mulgnn0ass  14590  odmulg  14863  torsubg  15140  isabvd  15579  prmirredlem  16440  nmo0  18238  nmoeq0  18239  blcvx  18298  reparphti  18489  pcorevlem  18518  ipcau2  18658  itg1addlem4  19048  itg1addlem5  19049  itg1mulc  19053  itg2mulc  19096  dvcmul  19287  dvmptcmul  19307  dvexp3  19319  dvef  19321  dveq0  19341  dv11cn  19342  ply1termlem  19579  plyeq0lem  19586  plypf1  19588  plyaddlem1  19589  plymullem1  19590  coeeulem  19600  coeidlem  19613  coeid3  19616  coemullem  19625  coemulhi  19629  coemulc  19630  dgrco  19650  vieta1lem2  19685  elqaalem2  19694  aalioulem3  19708  taylthlem2  19747  abelthlem6  19806  pilem2  19822  sinhalfpip  19854  sinhalfpim  19855  coshalfpip  19856  coshalfpim  19857  logtayl  20001  mulcxp  20026  cxpmul2  20030  cxpeq  20091  chordthmlem5  20127  cubic  20139  atans2  20221  atantayl2  20228  leibpi  20232  efrlim  20258  scvxcvx  20274  amgm  20279  ftalem5  20308  basellem2  20313  mumul  20413  muinv  20427  dchrn0  20483  dchrinvcl  20486  lgsdirnn0  20572  lgsdinn0  20573  lgsquad2lem2  20592  rpvmasumlem  20630  dchrisum0flblem1  20651  rpvmasum2  20655  ostth2lem2  20777  nvz0  21226  ipasslem1  21401  hi01  21667  subfacp1lem6  23120  cvxpcon  23177  cvxscon  23178  brbtwn2  23940  axsegconlem1  23952  axpaschlem  23975  axcontlem7  24005  axcontlem8  24006  pell1234qrne0  26337  bezoutr1  26472  jm2.19lem3  26483  jm2.25  26491  flcidc  26778  dvconstbi  26950  itgsinexplem1  27147
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511  ax-resscn 8789  ax-1cn 8790  ax-icn 8791  ax-addcl 8792  ax-addrcl 8793  ax-mulcl 8794  ax-mulrcl 8795  ax-mulcom 8796  ax-addass 8797  ax-mulass 8798  ax-distr 8799  ax-i2m1 8800  ax-1ne0 8801  ax-1rid 8802  ax-rnegex 8803  ax-rrecex 8804  ax-cnre 8805  ax-pre-lttri 8806  ax-pre-lttrn 8807  ax-pre-ltadd 8808
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-mpt 4080  df-id 4308  df-po 4313  df-so 4314  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-ov 5822  df-er 6655  df-en 6859  df-dom 6860  df-sdom 6861  df-pnf 8864  df-mnf 8865  df-ltxr 8867
  Copyright terms: Public domain W3C validator