Theorem mul01d 11397

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086  0cc0 11088   · cmul 11093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-po 5560  df-so 5561  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-ltxr 11236

This theorem is referenced by:  mulge0  11720  mul0or  11842  diveq0  11870  div0OLD  11894  lemul1a  12060  un0mulcl  12529  mul2lt0bi  13115  rexmul  13288  modid  13920  addmodlteq  13973  expmul  14134  sqlecan  14236  discr  14267  hashf1lem2  14483  hashf1  14484  sgnmul  15134  fsummulc2  15825  pwdif  15912  geolim  15914  geomulcvg  15920  fprodeq0  16019  0risefac  16082  0dvds  16324  smumullem  16540  bezoutlem1  16587  lcmgcd  16655  mulgcddvds  16703  cncongr2  16716  prmdiv  16834  pcaddlem  16938  qexpz  16951  prmreclem4  16969  prmreclem5  16970  mulgnn0ass  19167  odadd2  19910  isabvd  20884  nn0srg  21547  rge0srg  21548  pzriprnglem8  21598  mhppwdeg  22273  nmolb2d  24836  nmoleub  24849  reparphti  25117  pcorevlem  25146  itg1val2  25804  i1fmullem  25814  itg1addlem4  25819  itg10a  25830  itg1ge0a  25831  itg2const  25860  itg2monolem1  25870  itg0  25900  itgz  25901  iblmulc2  25951  itgmulc2lem1  25952  bddmulibl  25959  dvcnp2  26040  dvcobr  26066  dvlip  26113  dvlipcn  26114  c1lip1  26117  dvlt0  26125  plymullem1  26332  coefv0  26366  coemullem  26368  coemulhi  26372  dgrmulc  26389  dgrcolem2  26392  dvply1  26406  plydivlem3  26417  elqaalem2  26442  elqaalem3  26443  tayl0  26483  dvtaylp  26491  radcnv0  26537  dvradcnv  26542  pserdvlem2  26549  abelthlem2  26553  pilem2  26573  sinmpi  26610  cosmpi  26611  sinppi  26612  cosppi  26613  tanregt0  26662  efsubm  26674  argregt0  26733  argrege0  26734  argimgt0  26735  logtayl  26783  mulcxplem  26807  mulcxp  26808  cxpmul2  26812  pythag  26940  quad2  26962  dcubic  26969  atans2  27054  zetacvg  27137  lgamgulmlem2  27152  mumul  27303  logexprlim  27347  dchrsum2  27390  sumdchr2  27392  lgsdilem  27446  lgsdirnn0  27466  lgsdinn0  27467  lgsquad3  27509  2sqmod  27558  rpvmasumlem  27609  dchrisumlem1  27611  dchrvmasumiflem2  27624  rpvmasum2  27634  dchrisum0re  27635  pntrlog2bndlem4  27702  pntlemf  27727  pntleml  27733  ostth2lem2  27756  ostth3  27760  colinearalg  29169  nmlnoubi  31057  ipasslem2  31093  cdj3lem1  32695  oexpled  33093  constrrtlc2  34040  cos9thpiminplylem1  34089  cos9thpiminplylem2  34090  xrge0iifhom  34244  signsplypnf  34854  signswch  34865  signlem0  34891  itgexpif  34910  circlemeth  34944  knoppndvlem6  36968  knoppndvlem8  36970  knoppndvlem13  36975  ovoliunnfl  38173  voliunnfl  38175  itg2addnclem  38182  iblmulc2nc  38196  itgmulc2nclem1  38197  areacirc  38224  geomcau  38270  bfp  38335  lcmineqlem10  42667  lcmineqlem12  42669  irrapxlem1  43411  pell1qr1  43460  pell1qrgaplem  43462  rmxy0  43512  jm2.18  43577  mpaaeu  43739  relexpmulg  44298  binomcxplemnotnn0  44930  xralrple2  45928  stoweidlem26  46598  stoweidlem37  46609  stirlinglem7  46652  dirkercncflem2  46676  fourierdlem103  46781  fourierdlem104  46782  sqwvfoura  46800  sqwvfourb  46801  etransclem15  46821  etransclem24  46830  etransclem25  46831  etransclem32  46838  etransclem35  46841  etransclem48  46854  hoidmvlelem1  47167  hoidmvlelem2  47168  hoidmvlelem3  47169  sharhght  47437  altgsumbcALT  48984  dig0  49237  itcovalpclem1  49301  line2ylem  49382  line2xlem  49384  2itscp  49412