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

Theorem mul02d 10826
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 10806 . 2 (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
31, 2syl 17 1 (𝜑 → (0 · 𝐴) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523  0cc0 10525   · cmul 10530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-ltxr 10668
This theorem is referenced by:  mulneg1  11064  mulge0  11146  mul0or  11268  prodgt0  11475  un0mulcl  11919  mul2lt0rgt0  12480  mul2lt0bi  12483  lincmb01cmp  12869  iccf1o  12870  discr1  13588  discr  13589  hashxplem  13782  cshweqrep  14171  remul2  14477  immul2  14484  binomlem  15172  pwm1geoserOLD  15213  geomulcvg  15220  ntrivcvgfvn0  15243  fprodeq0  15317  fprodeq0g  15336  0fallfac  15379  binomfallfaclem2  15382  efne0  15438  dvds0  15613  pwp1fsum  15730  smumullem  15829  mulgcd  15884  bezoutr1  15901  lcmgcd  15939  qnumgt0  16078  pcexp  16184  vdwapun  16298  vdwlem1  16305  mulgnn0ass  18201  odmulg  18612  torsubg  18903  isabvd  19520  nn0srg  20543  rge0srg  20544  prmirredlem  20568  nmo0  23271  nmoeq0  23272  blcvx  23333  reparphti  23528  pcorevlem  23557  ipcau2  23764  rrxcph  23922  itg1addlem4  24227  itg1addlem5  24228  itg1mulc  24232  itg2mulc  24275  dvcmul  24468  dvmptcmul  24488  dvexp3  24502  dvef  24504  dveq0  24524  dv11cn  24525  ply1termlem  24720  plyeq0lem  24727  plypf1  24729  plyaddlem1  24730  plymullem1  24731  coeeulem  24741  coeidlem  24754  coeid3  24757  coemullem  24767  coemulhi  24771  coemulc  24772  dgrco  24792  vieta1lem2  24827  elqaalem2  24836  aalioulem3  24850  taylthlem2  24889  abelthlem6  24951  pilem2  24967  sinhalfpip  25005  sinhalfpim  25006  coshalfpip  25007  coshalfpim  25008  logtayl  25170  mulcxp  25195  cxpmul2  25199  cxpeq  25265  chordthmlem5  25341  cubic  25354  atans2  25436  atantayl2  25443  leibpi  25447  efrlim  25474  scvxcvx  25490  amgm  25495  ftalem5  25581  basellem2  25586  mumul  25685  muinv  25697  dchrn0  25753  dchrinvcl  25756  lgsdirnn0  25847  lgsdinn0  25848  lgsquad2lem2  25888  rpvmasumlem  25990  dchrisum0flblem1  26011  rpvmasum2  26015  ostth2lem2  26137  brbtwn2  26618  axsegconlem1  26630  axpaschlem  26653  axcontlem7  26683  axcontlem8  26684  elntg2  26698  nvz0  28372  ipasslem1  28535  hi01  28800  fprodeq02  30466  xrge0iifhom  31079  indsum  31179  indsumin  31180  eulerpartlemsv2  31515  eulerpartlems  31517  eulerpartlemsv3  31518  eulerpartlemgc  31519  eulerpartlemv  31521  eulerpartlemgs2  31537  sgnmul  31699  plymul02  31715  plymulx0  31716  itgexpif  31776  breprexplemc  31802  breprexp  31803  logdivsqrle  31820  subfacp1lem6  32329  cvxpconn  32386  cvxsconn  32387  fwddifnp1  33523  pell1234qrne0  39328  jm2.19lem3  39466  jm2.25  39474  flcidc  39652  relexpmulg  39933  radcnvrat  40523  dvconstbi  40543  binomcxplemnn0  40558  sineq0ALT  41148  fperiodmullem  41446  fprod0  41753  dvsinax  42073  dvasinbx  42081  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  dvnxpaek  42103  dvnmul  42104  itgsinexplem1  42115  dirkertrigeqlem2  42261  fourierdlem42  42311  fourierdlem83  42351  sqwvfoura  42390  fouriersw  42393  elaa2lem  42395  etransclem15  42411  etransclem24  42420  etransclem35  42431  etransclem46  42442  sigarcol  42998  sharhght  42999  fmtnofac2  43608  rrx2linest  44657  line2x  44669  line2y  44670  itschlc0yqe  44675  itschlc0xyqsol1  44681  itschlc0xyqsol  44682  2itscp  44696  aacllem  44830
  Copyright terms: Public domain W3C validator