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

Theorem mul02d 8890
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 8870 . 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 1619    e. wcel 1621  (class class class)co 5710   CCcc 8615   0cc0 8617    x. cmul 8622
This theorem is referenced by:  mulneg1  9096  mulge0  9171  mul0or  9288  prodgt0  9481  un0mulcl  9877  lincmb01cmp  10655  iccf1o  10656  discr1  11115  discr  11116  hashxplem  11262  remul2  11492  immul2  11499  binomlem  12164  geomulcvg  12206  efne0  12251  dvds0  12418  smumullem  12557  mulgcd  12599  qnumgt0  12695  pcexp  12786  vdwapun  12895  vdwlem1  12902  mulgnn0ass  14431  odmulg  14704  torsubg  14981  isabvd  15420  prmirredlem  16278  nmo0  18076  nmoeq0  18077  blcvx  18136  reparphti  18327  pcorevlem  18356  ipcau2  18496  itg1addlem4  18886  itg1addlem5  18887  itg1mulc  18891  itg2mulc  18934  dvcmul  19125  dvmptcmul  19145  dvexp3  19157  dvef  19159  dveq0  19179  dv11cn  19180  ply1termlem  19417  plyeq0lem  19424  plypf1  19426  plyaddlem1  19427  plymullem1  19428  coeeulem  19438  coeidlem  19451  coeid3  19454  coemullem  19463  coemulhi  19467  coemulc  19468  dgrco  19488  vieta1lem2  19523  elqaalem2  19532  aalioulem3  19546  taylthlem2  19585  abelthlem6  19644  pilem2  19660  sinhalfpip  19692  sinhalfpim  19693  coshalfpip  19694  coshalfpim  19695  logtayl  19839  chordthmlem5  19877  mulcxp  19900  cxpmul2  19904  cxpeq  19965  cubic  19977  atans2  20059  atantayl2  20066  leibpi  20070  efrlim  20096  scvxcvx  20112  amgm  20117  ftalem5  20146  basellem2  20151  mumul  20251  muinv  20265  dchrn0  20321  dchrinvcl  20324  lgsdirnn0  20410  lgsdinn0  20411  lgsquad2lem2  20430  rpvmasumlem  20468  dchrisum0flblem1  20489  rpvmasum2  20493  ostth2lem2  20615  nvz0  21064  ipasslem1  21239  hi01  21505  subfacp1lem6  22887  cvxpcon  22944  cvxscon  22945  brbtwn2  23707  axsegconlem1  23719  axpaschlem  23742  axcontlem7  23772  axcontlem8  23773  pell1234qrne0  26104  bezoutr1  26239  jm2.19lem3  26250  jm2.25  26258  flcidc  26545  dvconstbi  26717
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pow 4082  ax-pr 4108  ax-un 4403  ax-resscn 8674  ax-1cn 8675  ax-icn 8676  ax-addcl 8677  ax-addrcl 8678  ax-mulcl 8679  ax-mulrcl 8680  ax-mulcom 8681  ax-addass 8682  ax-mulass 8683  ax-distr 8684  ax-i2m1 8685  ax-1ne0 8686  ax-1rid 8687  ax-rnegex 8688  ax-rrecex 8689  ax-cnre 8690  ax-pre-lttri 8691  ax-pre-lttrn 8692  ax-pre-ltadd 8693
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-nel 2415  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-csb 3010  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-mpt 3976  df-id 4202  df-po 4207  df-so 4208  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fn 4603  df-f 4604  df-f1 4605  df-fo 4606  df-f1o 4607  df-fv 4608  df-ov 5713  df-er 6546  df-en 6750  df-dom 6751  df-sdom 6752  df-pnf 8749  df-mnf 8750  df-ltxr 8752
  Copyright terms: Public domain W3C validator