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

Theorem mul01d 9006
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 8986 . 2  |-  ( A  e.  CC  ->  ( A  x.  0 )  =  0 )
31, 2syl 17 1  |-  ( ph  ->  ( A  x.  0 )  =  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:  mulge0  9286  mul0or  9403  diveq0  9429  div0  9447  lemul1a  9605  un0mulcl  9993  rexmul  10585  modid  10987  expmul  11141  sqlecan  11203  discr  11232  hashf1lem2  11388  hashf1  11389  fsummulc2  12240  geolim  12320  geomulcvg  12326  0dvds  12543  smumullem  12677  bezoutlem1  12711  mulgcddvds  12777  prmdiv  12847  pcaddlem  12930  qexpz  12943  prmreclem4  12960  prmreclem5  12961  mulgnn0ass  14590  odadd2  15135  isabvd  15579  nmolb2d  18221  nmoleub  18234  reparphti  18489  pcorevlem  18518  itg1val2  19033  i1fmullem  19043  itg1addlem4  19048  itg10a  19059  itg1ge0a  19060  itg2const  19089  itg2monolem1  19099  itg0  19128  itgz  19129  iblmulc2  19179  itgmulc2lem1  19180  bddmulibl  19187  dvcnp2  19263  dvcobr  19289  dvlip  19334  dvlipcn  19335  c1lip1  19338  dvlt0  19346  plymullem1  19590  coefv0  19623  coemullem  19625  coemulhi  19629  dgrmulc  19646  dgrcolem2  19649  dvply1  19658  plydivlem3  19669  elqaalem2  19694  elqaalem3  19695  tayl0  19735  dvtaylp  19743  radcnv0  19786  dvradcnv  19791  pserdvlem2  19798  abelthlem2  19802  pilem2  19822  sinmpi  19849  cosmpi  19850  sinppi  19851  cosppi  19852  tanregt0  19895  argregt0  19958  argrege0  19959  argimgt0  19960  logtayl  20001  mulcxplem  20025  mulcxp  20026  cxpmul2  20030  pythag  20109  quad2  20129  dcubic  20136  atans2  20221  mumul  20413  logexprlim  20458  dchrsum2  20501  sumdchr2  20503  lgsdilem  20555  lgsdirnn0  20572  lgsdinn0  20573  lgsquad3  20594  rpvmasumlem  20630  dchrisumlem1  20632  dchrvmasumiflem2  20645  rpvmasum2  20655  dchrisum0re  20656  pntrlog2bndlem4  20723  pntlemf  20748  pntleml  20754  ostth2lem2  20777  ostth3  20781  gxnn0mul  20936  nmlnoubi  21366  ipasslem2  21402  cdj3lem1  23006  zetacvg  23093  colinearalg  23945  geomcau  25874  bfp  25947  irrapxlem1  26306  pell1qr1  26355  pell1qrgaplem  26357  rmxy0  26407  jm2.18  26480  mpaaeu  26754  stirlinglem7  27228
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