Theorem mul01d 11345

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  0cc0 11038   · cmul 11043

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184

This theorem is referenced by:  mulge0  11668  mul0or  11790  diveq0  11819  div0OLD  11843  lemul1a  12009  un0mulcl  12471  mul2lt0bi  13050  rexmul  13223  modid  13855  addmodlteq  13908  expmul  14069  sqlecan  14171  discr  14202  hashf1lem2  14418  hashf1  14419  fsummulc2  15746  pwdif  15833  geolim  15835  geomulcvg  15841  fprodeq0  15940  0risefac  16003  0dvds  16245  smumullem  16461  bezoutlem1  16508  lcmgcd  16576  mulgcddvds  16624  cncongr2  16637  prmdiv  16755  pcaddlem  16859  qexpz  16872  prmreclem4  16890  prmreclem5  16891  mulgnn0ass  19086  odadd2  19824  isabvd  20789  nn0srg  21417  rge0srg  21418  pzriprnglem8  21468  mhppwdeg  22116  nmolb2d  24683  nmoleub  24696  reparphti  24964  pcorevlem  24993  itg1val2  25651  i1fmullem  25661  itg1addlem4  25666  itg10a  25677  itg1ge0a  25678  itg2const  25707  itg2monolem1  25717  itg0  25747  itgz  25748  iblmulc2  25798  itgmulc2lem1  25799  bddmulibl  25806  dvcnp2  25887  dvcobr  25913  dvlip  25960  dvlipcn  25961  c1lip1  25964  dvlt0  25972  plymullem1  26179  coefv0  26213  coemullem  26215  coemulhi  26219  dgrmulc  26236  dgrcolem2  26239  dvply1  26250  plydivlem3  26261  elqaalem2  26286  elqaalem3  26287  tayl0  26327  dvtaylp  26335  radcnv0  26381  dvradcnv  26386  pserdvlem2  26393  abelthlem2  26397  pilem2  26417  sinmpi  26451  cosmpi  26452  sinppi  26453  cosppi  26454  tanregt0  26503  efsubm  26515  argregt0  26574  argrege0  26575  argimgt0  26576  logtayl  26624  mulcxplem  26648  mulcxp  26649  cxpmul2  26653  pythag  26781  quad2  26803  dcubic  26810  atans2  26895  zetacvg  26978  lgamgulmlem2  26993  mumul  27144  logexprlim  27188  dchrsum2  27231  sumdchr2  27233  lgsdilem  27287  lgsdirnn0  27307  lgsdinn0  27308  lgsquad3  27350  2sqmod  27399  rpvmasumlem  27450  dchrisumlem1  27452  dchrvmasumiflem2  27465  rpvmasum2  27475  dchrisum0re  27476  pntrlog2bndlem4  27543  pntlemf  27568  pntleml  27574  ostth2lem2  27597  ostth3  27601  colinearalg  28979  nmlnoubi  30867  ipasslem2  30903  cdj3lem1  32505  sgnmul  32908  oexpled  32920  constrrtlc2  33877  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  xrge0iifhom  34081  signsplypnf  34694  signswch  34705  signlem0  34731  itgexpif  34750  circlemeth  34784  knoppndvlem6  36777  knoppndvlem8  36779  knoppndvlem13  36784  ovoliunnfl  37983  voliunnfl  37985  itg2addnclem  37992  iblmulc2nc  38006  itgmulc2nclem1  38007  areacirc  38034  geomcau  38080  bfp  38145  lcmineqlem10  42477  lcmineqlem12  42479  irrapxlem1  43250  pell1qr1  43299  pell1qrgaplem  43301  rmxy0  43351  jm2.18  43416  mpaaeu  43578  relexpmulg  44137  binomcxplemnotnn0  44783  xralrple2  45784  stoweidlem26  46454  stoweidlem37  46465  stirlinglem7  46508  dirkercncflem2  46532  fourierdlem103  46637  fourierdlem104  46638  sqwvfoura  46656  sqwvfourb  46657  etransclem15  46677  etransclem24  46686  etransclem25  46687  etransclem32  46694  etransclem35  46697  etransclem48  46710  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  sharhght  47293  altgsumbcALT  48829  dig0  49082  itcovalpclem1  49146  line2ylem  49227  line2xlem  49229  2itscp  49257