Theorem mul01d 11460

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  0cc0 11155   · cmul 11160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300

This theorem is referenced by:  mulge0  11781  mul0or  11903  diveq0  11932  div0OLD  11956  lemul1a  12121  un0mulcl  12560  mul2lt0bi  13141  rexmul  13313  modid  13936  addmodlteq  13987  expmul  14148  sqlecan  14248  discr  14279  hashf1lem2  14495  hashf1  14496  fsummulc2  15820  pwdif  15904  geolim  15906  geomulcvg  15912  fprodeq0  16011  0risefac  16074  0dvds  16314  smumullem  16529  bezoutlem1  16576  lcmgcd  16644  mulgcddvds  16692  cncongr2  16705  prmdiv  16822  pcaddlem  16926  qexpz  16939  prmreclem4  16957  prmreclem5  16958  mulgnn0ass  19128  odadd2  19867  isabvd  20813  nn0srg  21455  rge0srg  21456  pzriprnglem8  21499  mhppwdeg  22154  nmolb2d  24739  nmoleub  24752  reparphti  25029  reparphtiOLD  25030  pcorevlem  25059  itg1val2  25719  i1fmullem  25729  itg1addlem4  25734  itg10a  25745  itg1ge0a  25746  itg2const  25775  itg2monolem1  25785  itg0  25815  itgz  25816  iblmulc2  25866  itgmulc2lem1  25867  bddmulibl  25874  dvcnp2  25955  dvcnp2OLD  25956  dvcobr  25983  dvcobrOLD  25984  dvlip  26032  dvlipcn  26033  c1lip1  26036  dvlt0  26044  plymullem1  26253  coefv0  26287  coemullem  26289  coemulhi  26293  dgrmulc  26311  dgrcolem2  26314  dvply1  26325  plydivlem3  26337  elqaalem2  26362  elqaalem3  26363  tayl0  26403  dvtaylp  26412  radcnv0  26459  dvradcnv  26464  pserdvlem2  26472  abelthlem2  26476  pilem2  26496  sinmpi  26529  cosmpi  26530  sinppi  26531  cosppi  26532  tanregt0  26581  efsubm  26593  argregt0  26652  argrege0  26653  argimgt0  26654  logtayl  26702  mulcxplem  26726  mulcxp  26727  cxpmul2  26731  pythag  26860  quad2  26882  dcubic  26889  atans2  26974  zetacvg  27058  lgamgulmlem2  27073  mumul  27224  logexprlim  27269  dchrsum2  27312  sumdchr2  27314  lgsdilem  27368  lgsdirnn0  27388  lgsdinn0  27389  lgsquad3  27431  2sqmod  27480  rpvmasumlem  27531  dchrisumlem1  27533  dchrvmasumiflem2  27546  rpvmasum2  27556  dchrisum0re  27557  pntrlog2bndlem4  27624  pntlemf  27649  pntleml  27655  ostth2lem2  27678  ostth3  27682  colinearalg  28925  nmlnoubi  30815  ipasslem2  30851  cdj3lem1  32453  constrrtlc2  33774  xrge0iifhom  33936  sgnmul  34545  signsplypnf  34565  signswch  34576  signlem0  34602  itgexpif  34621  circlemeth  34655  knoppndvlem6  36518  knoppndvlem8  36520  knoppndvlem13  36525  ovoliunnfl  37669  voliunnfl  37671  itg2addnclem  37678  iblmulc2nc  37692  itgmulc2nclem1  37693  areacirc  37720  geomcau  37766  bfp  37831  lcmineqlem10  42039  lcmineqlem12  42041  irrapxlem1  42833  pell1qr1  42882  pell1qrgaplem  42884  rmxy0  42935  jm2.18  43000  mpaaeu  43162  relexpmulg  43723  binomcxplemnotnn0  44375  xralrple2  45365  stoweidlem26  46041  stoweidlem37  46052  stirlinglem7  46095  dirkercncflem2  46119  fourierdlem103  46224  fourierdlem104  46225  sqwvfoura  46243  sqwvfourb  46244  etransclem15  46264  etransclem24  46273  etransclem25  46274  etransclem32  46281  etransclem35  46284  etransclem48  46297  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  sharhght  46880  altgsumbcALT  48269  dig0  48527  itcovalpclem1  48591  line2ylem  48672  line2xlem  48674  2itscp  48702