Theorem mul01d 11465

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  (class class class)co 7426  ℂcc 11158  0cc0 11160   · cmul 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5306  ax-nul 5313  ax-pow 5371  ax-pr 5435  ax-un 7748  ax-resscn 11217  ax-1cn 11218  ax-icn 11219  ax-addcl 11220  ax-addrcl 11221  ax-mulcl 11222  ax-mulrcl 11223  ax-mulcom 11224  ax-addass 11225  ax-mulass 11226  ax-distr 11227  ax-i2m1 11228  ax-1ne0 11229  ax-1rid 11230  ax-rnegex 11231  ax-rrecex 11232  ax-cnre 11233  ax-pre-lttri 11234  ax-pre-lttrn 11235  ax-pre-ltadd 11236

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-br 5156  df-opab 5218  df-mpt 5239  df-id 5582  df-po 5596  df-so 5597  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-ov 7429  df-er 8736  df-en 8977  df-dom 8978  df-sdom 8979  df-pnf 11302  df-mnf 11303  df-ltxr 11305

This theorem is referenced by:  mulge0  11784  mul0or  11906  diveq0  11935  div0  11955  lemul1a  12121  un0mulcl  12560  mul2lt0bi  13136  rexmul  13306  modid  13918  addmodlteq  13968  expmul  14129  sqlecan  14229  discr  14259  hashf1lem2  14477  hashf1  14478  fsummulc2  15790  pwdif  15874  geolim  15876  geomulcvg  15882  fprodeq0  15979  0risefac  16042  0dvds  16281  smumullem  16494  bezoutlem1  16542  lcmgcd  16610  mulgcddvds  16658  cncongr2  16671  prmdiv  16789  pcaddlem  16892  qexpz  16905  prmreclem4  16923  prmreclem5  16924  mulgnn0ass  19106  odadd2  19849  isabvd  20793  nn0srg  21436  rge0srg  21437  pzriprnglem8  21480  mhppwdeg  22146  nmolb2d  24729  nmoleub  24742  reparphti  25017  reparphtiOLD  25018  pcorevlem  25047  itg1val2  25707  i1fmullem  25717  itg1addlem4  25722  itg1addlem4OLD  25723  itg10a  25734  itg1ge0a  25735  itg2const  25764  itg2monolem1  25774  itg0  25803  itgz  25804  iblmulc2  25854  itgmulc2lem1  25855  bddmulibl  25862  dvcnp2  25943  dvcnp2OLD  25944  dvcobr  25971  dvcobrOLD  25972  dvlip  26020  dvlipcn  26021  c1lip1  26024  dvlt0  26032  plymullem1  26244  coefv0  26278  coemullem  26280  coemulhi  26284  dgrmulc  26302  dgrcolem2  26305  dvply1  26314  plydivlem3  26326  elqaalem2  26351  elqaalem3  26352  tayl0  26392  dvtaylp  26401  radcnv0  26448  dvradcnv  26453  pserdvlem2  26461  abelthlem2  26465  pilem2  26485  sinmpi  26518  cosmpi  26519  sinppi  26520  cosppi  26521  tanregt0  26569  efsubm  26581  argregt0  26640  argrege0  26641  argimgt0  26642  logtayl  26690  mulcxplem  26714  mulcxp  26715  cxpmul2  26719  pythag  26848  quad2  26870  dcubic  26877  atans2  26962  zetacvg  27046  lgamgulmlem2  27061  mumul  27212  logexprlim  27257  dchrsum2  27300  sumdchr2  27302  lgsdilem  27356  lgsdirnn0  27376  lgsdinn0  27377  lgsquad3  27419  2sqmod  27468  rpvmasumlem  27519  dchrisumlem1  27521  dchrvmasumiflem2  27534  rpvmasum2  27544  dchrisum0re  27545  pntrlog2bndlem4  27612  pntlemf  27637  pntleml  27643  ostth2lem2  27666  ostth3  27670  colinearalg  28847  nmlnoubi  30732  ipasslem2  30768  cdj3lem1  32370  xrge0iifhom  33754  sgnmul  34378  signsplypnf  34398  signswch  34409  signlem0  34435  itgexpif  34454  circlemeth  34488  knoppndvlem6  36222  knoppndvlem8  36224  knoppndvlem13  36229  ovoliunnfl  37365  voliunnfl  37367  itg2addnclem  37374  iblmulc2nc  37388  itgmulc2nclem1  37389  areacirc  37416  geomcau  37462  bfp  37527  lcmineqlem10  41739  lcmineqlem12  41741  irrapxlem1  42497  pell1qr1  42546  pell1qrgaplem  42548  rmxy0  42599  jm2.18  42664  mpaaeu  42829  relexpmulg  43395  binomcxplemnotnn0  44048  xralrple2  44987  stoweidlem26  45665  stoweidlem37  45676  stirlinglem7  45719  dirkercncflem2  45743  fourierdlem103  45848  fourierdlem104  45849  sqwvfoura  45867  sqwvfourb  45868  etransclem15  45888  etransclem24  45897  etransclem25  45898  etransclem32  45905  etransclem35  45908  etransclem48  45921  hoidmvlelem1  46234  hoidmvlelem2  46235  hoidmvlelem3  46236  sharhght  46504  altgsumbcALT  47750  dig0  48012  itcovalpclem1  48076  line2ylem  48157  line2xlem  48159  2itscp  48187