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

Theorem mul02d 9820
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 9800 . 2  |-  ( A  e.  CC  ->  (
0  x.  A )  =  0 )
31, 2syl 17 1  |-  ( ph  ->  ( 0  x.  A
)  =  0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1867  (class class class)co 6296   CCcc 9526   0cc0 9528    x. cmul 9533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-po 4766  df-so 4767  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-ov 6299  df-er 7362  df-en 7569  df-dom 7570  df-sdom 7571  df-pnf 9666  df-mnf 9667  df-ltxr 9669
This theorem is referenced by:  mulneg1  10044  mulge0  10121  mul0or  10241  prodgt0  10439  un0mulcl  10893  mul2lt0rgt0  11388  mul2lt0bi  11391  lincmb01cmp  11762  iccf1o  11763  discr1  12394  discr  12395  hashxplem  12589  cshweqrep  12894  remul2  13161  immul2  13168  binomlem  13854  geomulcvg  13899  ntrivcvgfvn0  13922  fprodeq0  13996  fprodeq0g  14015  0fallfac  14057  binomfallfaclem2  14060  efne0  14118  dvds0  14285  mulmoddvds  14330  smumullem  14429  mulgcd  14474  lcmgcd  14532  qnumgt0  14659  pcexp  14761  vdwapun  14876  vdwlem1  14883  mulgnn0ass  16731  odmulg  17138  torsubg  17420  isabvd  17976  nn0srg  18964  rge0srg  18965  prmirredlem  18988  nmo0  21680  nmoeq0  21681  blcvx  21740  reparphti  21934  pcorevlem  21963  ipcau2  22114  rrxcph  22257  itg1addlem4  22551  itg1addlem5  22552  itg1mulc  22556  itg2mulc  22599  dvcmul  22792  dvmptcmul  22812  dvexp3  22824  dvef  22826  dveq0  22846  dv11cn  22847  ply1termlem  23051  plyeq0lem  23058  plypf1  23060  plyaddlem1  23061  plymullem1  23062  coeeulem  23072  coeidlem  23085  coeid3  23088  coemullem  23098  coemulhi  23102  coemulc  23103  dgrco  23123  vieta1lem2  23158  elqaalem2  23167  aalioulem3  23181  taylthlem2  23220  abelthlem6  23282  pilem2  23298  pilem2OLD  23299  sinhalfpip  23338  sinhalfpim  23339  coshalfpip  23340  coshalfpim  23341  logtayl  23496  mulcxp  23521  cxpmul2  23525  cxpeq  23588  chordthmlem5  23653  cubic  23666  atans2  23748  atantayl2  23755  leibpi  23759  efrlim  23786  scvxcvx  23802  amgm  23807  ftalem5  23892  basellem2  23897  mumul  23997  muinv  24011  dchrn0  24067  dchrinvcl  24070  lgsdirnn0  24156  lgsdinn0  24157  lgsquad2lem2  24176  rpvmasumlem  24214  dchrisum0flblem1  24235  rpvmasum2  24239  ostth2lem2  24361  brbtwn2  24807  axsegconlem1  24819  axpaschlem  24842  axcontlem7  24872  axcontlem8  24873  nvz0  26168  ipasslem1  26343  hi01  26610  xrge0iifhom  28608  indsum  28709  eulerpartlemsv2  29043  eulerpartlems  29045  eulerpartlemsv3  29046  eulerpartlemgc  29047  eulerpartlemv  29049  eulerpartlemgs2  29065  sgnmul  29227  plymul02  29249  plymulx0  29250  subfacp1lem6  29722  cvxpcon  29779  cvxscon  29780  fwddifnp1  30743  pell1234qrne0  35438  bezoutr1  35575  jm2.19lem3  35585  jm2.25  35593  flcidc  35772  relexpmulg  35974  radcnvrat  36333  dvconstbi  36353  binomcxplemnn0  36368  sineq0ALT  37007  fperiodmullem  37163  fprod0  37281  dvsinax  37388  dvasinbx  37397  ioodvbdlimc1lem2  37409  ioodvbdlimc2lem  37411  dvnxpaek  37419  dvnmul  37420  itgsinexplem1  37432  dirkertrigeqlem2  37563  fourierdlem42  37613  fourierdlem83  37654  sqwvfoura  37693  fouriersw  37696  elaa2lem  37698  etransclem15  37714  etransclem24  37723  etransclem35  37734  etransclem46  37745  sigarcol  37906  sharhght  37907  aacllem  39343
  Copyright terms: Public domain W3C validator