Theorem mul01d 11336

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
mul01d	⊢ (𝜑 → (𝐴 · 0) = 0)

Proof of Theorem mul01d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mul01 11316	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 · 0) = 0)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027  0cc0 11029   · cmul 11034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-ltxr 11175

This theorem is referenced by:  mulge0  11659  mul0or  11781  diveq0  11810  div0OLD  11834  lemul1a  12000  un0mulcl  12462  mul2lt0bi  13041  rexmul  13214  modid  13846  addmodlteq  13899  expmul  14060  sqlecan  14162  discr  14193  hashf1lem2  14409  hashf1  14410  fsummulc2  15737  pwdif  15824  geolim  15826  geomulcvg  15832  fprodeq0  15931  0risefac  15994  0dvds  16236  smumullem  16452  bezoutlem1  16499  lcmgcd  16567  mulgcddvds  16615  cncongr2  16628  prmdiv  16746  pcaddlem  16850  qexpz  16863  prmreclem4  16881  prmreclem5  16882  mulgnn0ass  19077  odadd2  19815  isabvd  20780  nn0srg  21427  rge0srg  21428  pzriprnglem8  21478  mhppwdeg  22126  nmolb2d  24693  nmoleub  24706  reparphti  24974  pcorevlem  25003  itg1val2  25661  i1fmullem  25671  itg1addlem4  25676  itg10a  25687  itg1ge0a  25688  itg2const  25717  itg2monolem1  25727  itg0  25757  itgz  25758  iblmulc2  25808  itgmulc2lem1  25809  bddmulibl  25816  dvcnp2  25897  dvcobr  25923  dvlip  25970  dvlipcn  25971  c1lip1  25974  dvlt0  25982  plymullem1  26189  coefv0  26223  coemullem  26225  coemulhi  26229  dgrmulc  26246  dgrcolem2  26249  dvply1  26260  plydivlem3  26272  elqaalem2  26297  elqaalem3  26298  tayl0  26338  dvtaylp  26347  radcnv0  26394  dvradcnv  26399  pserdvlem2  26406  abelthlem2  26410  pilem2  26430  sinmpi  26464  cosmpi  26465  sinppi  26466  cosppi  26467  tanregt0  26516  efsubm  26528  argregt0  26587  argrege0  26588  argimgt0  26589  logtayl  26637  mulcxplem  26661  mulcxp  26662  cxpmul2  26666  pythag  26794  quad2  26816  dcubic  26823  atans2  26908  zetacvg  26992  lgamgulmlem2  27007  mumul  27158  logexprlim  27202  dchrsum2  27245  sumdchr2  27247  lgsdilem  27301  lgsdirnn0  27321  lgsdinn0  27322  lgsquad3  27364  2sqmod  27413  rpvmasumlem  27464  dchrisumlem1  27466  dchrvmasumiflem2  27479  rpvmasum2  27489  dchrisum0re  27490  pntrlog2bndlem4  27557  pntlemf  27582  pntleml  27588  ostth2lem2  27611  ostth3  27615  colinearalg  28993  nmlnoubi  30882  ipasslem2  30918  cdj3lem1  32520  sgnmul  32923  oexpled  32935  constrrtlc2  33893  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  xrge0iifhom  34097  signsplypnf  34710  signswch  34721  signlem0  34747  itgexpif  34766  circlemeth  34800  knoppndvlem6  36793  knoppndvlem8  36795  knoppndvlem13  36800  ovoliunnfl  37997  voliunnfl  37999  itg2addnclem  38006  iblmulc2nc  38020  itgmulc2nclem1  38021  areacirc  38048  geomcau  38094  bfp  38159  lcmineqlem10  42491  lcmineqlem12  42493  irrapxlem1  43268  pell1qr1  43317  pell1qrgaplem  43319  rmxy0  43369  jm2.18  43434  mpaaeu  43596  relexpmulg  44155  binomcxplemnotnn0  44801  xralrple2  45802  stoweidlem26  46472  stoweidlem37  46483  stirlinglem7  46526  dirkercncflem2  46550  fourierdlem103  46655  fourierdlem104  46656  sqwvfoura  46674  sqwvfourb  46675  etransclem15  46695  etransclem24  46704  etransclem25  46705  etransclem32  46712  etransclem35  46715  etransclem48  46728  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  sharhght  47311  altgsumbcALT  48841  dig0  49094  itcovalpclem1  49158  line2ylem  49239  line2xlem  49241  2itscp  49269