Theorem mul01d 11344

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂ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 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  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 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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183

This theorem is referenced by:  mulge0  11667  mul0or  11789  diveq0  11818  div0OLD  11842  lemul1a  12007  un0mulcl  12447  mul2lt0bi  13025  rexmul  13198  modid  13828  addmodlteq  13881  expmul  14042  sqlecan  14144  discr  14175  hashf1lem2  14391  hashf1  14392  fsummulc2  15719  pwdif  15803  geolim  15805  geomulcvg  15811  fprodeq0  15910  0risefac  15973  0dvds  16215  smumullem  16431  bezoutlem1  16478  lcmgcd  16546  mulgcddvds  16594  cncongr2  16607  prmdiv  16724  pcaddlem  16828  qexpz  16841  prmreclem4  16859  prmreclem5  16860  mulgnn0ass  19052  odadd2  19790  isabvd  20757  nn0srg  21404  rge0srg  21405  pzriprnglem8  21455  mhppwdeg  22105  nmolb2d  24674  nmoleub  24687  reparphti  24964  reparphtiOLD  24965  pcorevlem  24994  itg1val2  25653  i1fmullem  25663  itg1addlem4  25668  itg10a  25679  itg1ge0a  25680  itg2const  25709  itg2monolem1  25719  itg0  25749  itgz  25750  iblmulc2  25800  itgmulc2lem1  25801  bddmulibl  25808  dvcnp2  25889  dvcnp2OLD  25890  dvcobr  25917  dvcobrOLD  25918  dvlip  25966  dvlipcn  25967  c1lip1  25970  dvlt0  25978  plymullem1  26187  coefv0  26221  coemullem  26223  coemulhi  26227  dgrmulc  26245  dgrcolem2  26248  dvply1  26259  plydivlem3  26271  elqaalem2  26296  elqaalem3  26297  tayl0  26337  dvtaylp  26346  radcnv0  26393  dvradcnv  26398  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  26795  quad2  26817  dcubic  26824  atans2  26909  zetacvg  26993  lgamgulmlem2  27008  mumul  27159  logexprlim  27204  dchrsum2  27247  sumdchr2  27249  lgsdilem  27303  lgsdirnn0  27323  lgsdinn0  27324  lgsquad3  27366  2sqmod  27415  rpvmasumlem  27466  dchrisumlem1  27468  dchrvmasumiflem2  27481  rpvmasum2  27491  dchrisum0re  27492  pntrlog2bndlem4  27559  pntlemf  27584  pntleml  27590  ostth2lem2  27613  ostth3  27617  colinearalg  28995  nmlnoubi  30883  ipasslem2  30919  cdj3lem1  32521  sgnmul  32926  oexpled  32938  constrrtlc2  33910  cos9thpiminplylem1  33959  cos9thpiminplylem2  33960  xrge0iifhom  34114  signsplypnf  34727  signswch  34738  signlem0  34764  itgexpif  34783  circlemeth  34817  knoppndvlem6  36736  knoppndvlem8  36738  knoppndvlem13  36743  ovoliunnfl  37907  voliunnfl  37909  itg2addnclem  37916  iblmulc2nc  37930  itgmulc2nclem1  37931  areacirc  37958  geomcau  38004  bfp  38069  lcmineqlem10  42402  lcmineqlem12  42404  irrapxlem1  43173  pell1qr1  43222  pell1qrgaplem  43224  rmxy0  43274  jm2.18  43339  mpaaeu  43501  relexpmulg  44060  binomcxplemnotnn0  44706  xralrple2  45707  stoweidlem26  46378  stoweidlem37  46389  stirlinglem7  46432  dirkercncflem2  46456  fourierdlem103  46561  fourierdlem104  46562  sqwvfoura  46580  sqwvfourb  46581  etransclem15  46601  etransclem24  46610  etransclem25  46611  etransclem32  46618  etransclem35  46621  etransclem48  46634  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  sharhght  47217  altgsumbcALT  48707  dig0  48960  itcovalpclem1  49024  line2ylem  49105  line2xlem  49107  2itscp  49135