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

Theorem mul02d 8964
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 8944 . 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 5778   CCcc 8689   0cc0 8691    x. cmul 8696
This theorem is referenced by:  mulneg1  9170  mulge0  9245  mul0or  9362  prodgt0  9555  un0mulcl  9951  lincmb01cmp  10729  iccf1o  10730  discr1  11189  discr  11190  hashxplem  11336  remul2  11566  immul2  11573  binomlem  12238  geomulcvg  12280  efne0  12325  dvds0  12492  smumullem  12631  mulgcd  12673  qnumgt0  12769  pcexp  12860  vdwapun  12969  vdwlem1  12976  mulgnn0ass  14544  odmulg  14817  torsubg  15094  isabvd  15533  prmirredlem  16394  nmo0  18192  nmoeq0  18193  blcvx  18252  reparphti  18443  pcorevlem  18472  ipcau2  18612  itg1addlem4  19002  itg1addlem5  19003  itg1mulc  19007  itg2mulc  19050  dvcmul  19241  dvmptcmul  19261  dvexp3  19273  dvef  19275  dveq0  19295  dv11cn  19296  ply1termlem  19533  plyeq0lem  19540  plypf1  19542  plyaddlem1  19543  plymullem1  19544  coeeulem  19554  coeidlem  19567  coeid3  19570  coemullem  19579  coemulhi  19583  coemulc  19584  dgrco  19604  vieta1lem2  19639  elqaalem2  19648  aalioulem3  19662  taylthlem2  19701  abelthlem6  19760  pilem2  19776  sinhalfpip  19808  sinhalfpim  19809  coshalfpip  19810  coshalfpim  19811  logtayl  19955  mulcxp  19980  cxpmul2  19984  cxpeq  20045  chordthmlem5  20081  cubic  20093  atans2  20175  atantayl2  20182  leibpi  20186  efrlim  20212  scvxcvx  20228  amgm  20233  ftalem5  20262  basellem2  20267  mumul  20367  muinv  20381  dchrn0  20437  dchrinvcl  20440  lgsdirnn0  20526  lgsdinn0  20527  lgsquad2lem2  20546  rpvmasumlem  20584  dchrisum0flblem1  20605  rpvmasum2  20609  ostth2lem2  20731  nvz0  21180  ipasslem1  21355  hi01  21621  subfacp1lem6  23074  cvxpcon  23131  cvxscon  23132  brbtwn2  23894  axsegconlem1  23906  axpaschlem  23929  axcontlem7  23959  axcontlem8  23960  pell1234qrne0  26291  bezoutr1  26426  jm2.19lem3  26437  jm2.25  26445  flcidc  26732  dvconstbi  26904
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 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pow 4146  ax-pr 4172  ax-un 4470  ax-resscn 8748  ax-1cn 8749  ax-icn 8750  ax-addcl 8751  ax-addrcl 8752  ax-mulcl 8753  ax-mulrcl 8754  ax-mulcom 8755  ax-addass 8756  ax-mulass 8757  ax-distr 8758  ax-i2m1 8759  ax-1ne0 8760  ax-1rid 8761  ax-rnegex 8762  ax-rrecex 8763  ax-cnre 8764  ax-pre-lttri 8765  ax-pre-lttrn 8766  ax-pre-ltadd 8767
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 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-nel 2422  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-sbc 2953  df-csb 3043  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-mpt 4039  df-id 4267  df-po 4272  df-so 4273  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fun 4669  df-fn 4670  df-f 4671  df-f1 4672  df-fo 4673  df-f1o 4674  df-fv 4675  df-ov 5781  df-er 6614  df-en 6818  df-dom 6819  df-sdom 6820  df-pnf 8823  df-mnf 8824  df-ltxr 8826
  Copyright terms: Public domain W3C validator