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

Theorem mul02d 10827
Description: Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
mul02d (𝜑 → (0 · 𝐴) = 0)

Proof of Theorem mul02d
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 mul02 10807 . 2 (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
31, 2syl 17 1 (𝜑 → (0 · 𝐴) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  (class class class)co 7148  cc 10524  0cc0 10526   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-po 5473  df-so 5474  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-ov 7151  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-ltxr 10669
This theorem is referenced by:  mulneg1  11065  mulge0  11147  mul0or  11269  prodgt0  11476  un0mulcl  11920  mul2lt0rgt0  12482  mul2lt0bi  12485  lincmb01cmp  12871  iccf1o  12872  discr1  13590  discr  13591  hashxplem  13784  cshweqrep  14173  remul2  14479  immul2  14486  binomlem  15174  pwm1geoserOLD  15215  geomulcvg  15222  ntrivcvgfvn0  15245  fprodeq0  15319  fprodeq0g  15338  0fallfac  15381  binomfallfaclem2  15384  efne0  15440  dvds0  15615  pwp1fsum  15732  smumullem  15831  mulgcd  15886  bezoutr1  15903  lcmgcd  15941  qnumgt0  16080  pcexp  16186  vdwapun  16300  vdwlem1  16307  mulgnn0ass  18193  odmulg  18603  torsubg  18894  isabvd  19511  nn0srg  20531  rge0srg  20532  prmirredlem  20556  nmo0  23259  nmoeq0  23260  blcvx  23321  reparphti  23516  pcorevlem  23545  ipcau2  23752  rrxcph  23910  itg1addlem4  24215  itg1addlem5  24216  itg1mulc  24220  itg2mulc  24263  dvcmul  24456  dvmptcmul  24476  dvexp3  24490  dvef  24492  dveq0  24512  dv11cn  24513  ply1termlem  24708  plyeq0lem  24715  plypf1  24717  plyaddlem1  24718  plymullem1  24719  coeeulem  24729  coeidlem  24742  coeid3  24745  coemullem  24755  coemulhi  24759  coemulc  24760  dgrco  24780  vieta1lem2  24815  elqaalem2  24824  aalioulem3  24838  taylthlem2  24877  abelthlem6  24939  pilem2  24955  sinhalfpip  24993  sinhalfpim  24994  coshalfpip  24995  coshalfpim  24996  logtayl  25156  mulcxp  25181  cxpmul2  25185  cxpeq  25251  chordthmlem5  25327  cubic  25340  atans2  25422  atantayl2  25429  leibpi  25434  efrlim  25461  scvxcvx  25477  amgm  25482  ftalem5  25568  basellem2  25573  mumul  25672  muinv  25684  dchrn0  25740  dchrinvcl  25743  lgsdirnn0  25834  lgsdinn0  25835  lgsquad2lem2  25875  rpvmasumlem  25977  dchrisum0flblem1  25998  rpvmasum2  26002  ostth2lem2  26124  brbtwn2  26605  axsegconlem1  26617  axpaschlem  26640  axcontlem7  26670  axcontlem8  26671  elntg2  26685  nvz0  28359  ipasslem1  28522  hi01  28787  fprodeq02  30453  xrge0iifhom  31066  indsum  31166  indsumin  31167  eulerpartlemsv2  31502  eulerpartlems  31504  eulerpartlemsv3  31505  eulerpartlemgc  31506  eulerpartlemv  31508  eulerpartlemgs2  31524  sgnmul  31686  plymul02  31702  plymulx0  31703  itgexpif  31763  breprexplemc  31789  breprexp  31790  logdivsqrle  31807  subfacp1lem6  32316  cvxpconn  32373  cvxsconn  32374  fwddifnp1  33510  pell1234qrne0  39315  jm2.19lem3  39453  jm2.25  39461  flcidc  39639  relexpmulg  39920  radcnvrat  40511  dvconstbi  40531  binomcxplemnn0  40546  sineq0ALT  41136  fperiodmullem  41435  fprod0  41742  dvsinax  42062  dvasinbx  42070  ioodvbdlimc1lem2  42082  ioodvbdlimc2lem  42084  dvnxpaek  42092  dvnmul  42093  itgsinexplem1  42104  dirkertrigeqlem2  42250  fourierdlem42  42300  fourierdlem83  42340  sqwvfoura  42379  fouriersw  42382  elaa2lem  42384  etransclem15  42400  etransclem24  42409  etransclem35  42420  etransclem46  42431  sigarcol  42987  sharhght  42988  fmtnofac2  43563  rrx2linest  44561  line2x  44573  line2y  44574  itschlc0yqe  44579  itschlc0xyqsol1  44585  itschlc0xyqsol  44586  2itscp  44600  aacllem  44734
  Copyright terms: Public domain W3C validator