Theorem mul01d 11343

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 11323	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 · 0) = 0)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 · 0) = 0)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034  0cc0 11036   · cmul 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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 7366  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-ltxr 11182

This theorem is referenced by:  mulge0  11666  mul0or  11788  diveq0  11817  div0OLD  11841  lemul1a  12007  un0mulcl  12469  mul2lt0bi  13048  rexmul  13221  modid  13853  addmodlteq  13906  expmul  14067  sqlecan  14169  discr  14200  hashf1lem2  14416  hashf1  14417  fsummulc2  15744  pwdif  15831  geolim  15833  geomulcvg  15839  fprodeq0  15938  0risefac  16001  0dvds  16243  smumullem  16459  bezoutlem1  16506  lcmgcd  16574  mulgcddvds  16622  cncongr2  16635  prmdiv  16753  pcaddlem  16857  qexpz  16870  prmreclem4  16888  prmreclem5  16889  mulgnn0ass  19084  odadd2  19822  isabvd  20791  nn0srg  21419  rge0srg  21420  pzriprnglem8  21470  mhppwdeg  22145  nmolb2d  24708  nmoleub  24721  reparphti  24989  pcorevlem  25018  itg1val2  25676  i1fmullem  25686  itg1addlem4  25691  itg10a  25702  itg1ge0a  25703  itg2const  25732  itg2monolem1  25742  itg0  25772  itgz  25773  iblmulc2  25823  itgmulc2lem1  25824  bddmulibl  25831  dvcnp2  25912  dvcobr  25938  dvlip  25985  dvlipcn  25986  c1lip1  25989  dvlt0  25997  plymullem1  26204  coefv0  26238  coemullem  26240  coemulhi  26244  dgrmulc  26261  dgrcolem2  26264  dvply1  26275  plydivlem3  26286  elqaalem2  26311  elqaalem3  26312  tayl0  26352  dvtaylp  26360  radcnv0  26406  dvradcnv  26411  pserdvlem2  26418  abelthlem2  26422  pilem2  26442  sinmpi  26476  cosmpi  26477  sinppi  26478  cosppi  26479  tanregt0  26528  efsubm  26540  argregt0  26599  argrege0  26600  argimgt0  26601  logtayl  26649  mulcxplem  26673  mulcxp  26674  cxpmul2  26678  pythag  26806  quad2  26828  dcubic  26835  atans2  26920  zetacvg  27003  lgamgulmlem2  27018  mumul  27169  logexprlim  27213  dchrsum2  27256  sumdchr2  27258  lgsdilem  27312  lgsdirnn0  27332  lgsdinn0  27333  lgsquad3  27375  2sqmod  27424  rpvmasumlem  27475  dchrisumlem1  27477  dchrvmasumiflem2  27490  rpvmasum2  27500  dchrisum0re  27501  pntrlog2bndlem4  27568  pntlemf  27593  pntleml  27599  ostth2lem2  27622  ostth3  27626  colinearalg  29004  nmlnoubi  30892  ipasslem2  30928  cdj3lem1  32530  sgnmul  32934  oexpled  32946  constrrtlc2  33924  cos9thpiminplylem1  33973  cos9thpiminplylem2  33974  xrge0iifhom  34128  signsplypnf  34741  signswch  34752  signlem0  34778  itgexpif  34797  circlemeth  34831  knoppndvlem6  36830  knoppndvlem8  36832  knoppndvlem13  36837  ovoliunnfl  38036  voliunnfl  38038  itg2addnclem  38045  iblmulc2nc  38059  itgmulc2nclem1  38060  areacirc  38087  geomcau  38133  bfp  38198  lcmineqlem10  42530  lcmineqlem12  42532  irrapxlem1  43274  pell1qr1  43323  pell1qrgaplem  43325  rmxy0  43375  jm2.18  43440  mpaaeu  43602  relexpmulg  44161  binomcxplemnotnn0  44807  xralrple2  45806  stoweidlem26  46476  stoweidlem37  46487  stirlinglem7  46530  dirkercncflem2  46554  fourierdlem103  46659  fourierdlem104  46660  sqwvfoura  46678  sqwvfourb  46679  etransclem15  46699  etransclem24  46708  etransclem25  46709  etransclem32  46716  etransclem35  46719  etransclem48  46732  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  sharhght  47315  altgsumbcALT  48851  dig0  49104  itcovalpclem1  49168  line2ylem  49249  line2xlem  49251  2itscp  49279