Theorem mul01d 11512

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201  0cc0 11203   · cmul 11208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-er 8720  df-en 8977  df-dom 8978  df-sdom 8979  df-pnf 11348  df-mnf 11349  df-ltxr 11351

This theorem is used by:  mulge0  11837  mul0or  11959  diveq0  11987  lemul1a  12174  un0mulcl  12643  mul2lt0bi  13231  rexmul  13404  modid  14039  addmodlteq  14092  expmul  14253  sqlecan  14356  discr  14387  hashf1lem2  14604  hashf1  14605  sgnmul  15265  fsummulc2  15955  pwdif  16042  geolim  16044  geomulcvg  16050  fprodeq0  16147  0risefac  16209  0dvds  16451  smumullem  16667  bezoutlem1  16717  lcmgcd  16787  mulgcddvds  16835  cncongr2  16848  prmdiv  16967  pcaddlem  17071  qexpz  17084  prmreclem4  17102  prmreclem5  17103  mulgnn0ass  19325  odadd2  20068  isabvd  21074  nn0srg  21748  rge0srg  21749  pzriprnglem8  21799  mhppwdeg  22476  nmolb2d  25042  nmoleub  25055  reparphti  25323  pcorevlem  25352  itg1val2  26010  i1fmullem  26020  itg1addlem4  26025  itg10a  26036  itg1ge0a  26037  itg2const  26066  itg2monolem1  26076  itg0  26105  itgz  26106  iblmulc2  26156  itgmulc2lem1  26157  bddmulibl  26164  dvcnp2  26245  dvcobr  26271  dvlip  26318  dvlipcn  26319  c1lip1  26322  dvlt0  26330  plymullem1  26538  coefv0  26572  coemullem  26574  coemulhi  26578  dgrmulc  26595  dgrcolem2  26598  dvply1  26610  plydivlem3  26621  elqaalem2  26648  elqaalem3  26649  tayl0  26694  dvtaylp  26702  radcnv0  26748  dvradcnv  26753  pserdvlem2  26760  abelthlem2  26764  pilem2  26784  sinmpi  26821  cosmpi  26822  sinppi  26823  cosppi  26824  tanregt0  26872  efsubm  26884  argregt0  26943  argrege0  26944  argimgt0  26945  logtayl  26993  mulcxplem  27017  mulcxp  27018  cxpmul2  27022  pythag  27150  quad2  27172  dcubic  27179  atans2  27264  zetacvg  27347  lgamgulmlem2  27362  mumul  27513  logexprlim  27557  dchrsum2  27600  sumdchr2  27602  lgsdilem  27656  lgsdirnn0  27676  lgsdinn0  27677  lgsquad3  27719  2sqmod  27768  rpvmasumlem  27819  dchrisumlem1  27821  dchrvmasumiflem2  27834  rpvmasum2  27844  dchrisum0re  27845  pntrlog2bndlem4  27912  pntlemf  27937  pntleml  27943  ostth2lem2  27966  ostth3  27970  colinearalg  29493  nmlnoubi  31403  ipasslem2  31439  cdj3lem1  33041  oexpled  33473  constrrtlc2  34411  cos9thpiminplylem1  34460  cos9thpiminplylem2  34461  xrge0iifhom  34615  signsplypnf  35225  signswch  35236  signlem0  35262  itgexpif  35281  circlemeth  35315  knoppndvlem6  37475  knoppndvlem8  37477  knoppndvlem13  37482  ovoliunnfl  38673  voliunnfl  38675  itg2addnclem  38682  iblmulc2nc  38696  itgmulc2nclem1  38697  areacirc  38724  geomcau  38786  bfp  38851  lcmineqlem10  43181  lcmineqlem12  43183  irrapxlem1  43922  pell1qr1  43971  pell1qrgaplem  43973  rmxy0  44023  jm2.18  44088  mpaaeu  44245  relexpmulg  44803  binomcxplemnotnn0  45433  xralrple2  46459  stoweidlem26  47129  stoweidlem37  47140  stirlinglem7  47183  dirkercncflem2  47207  fourierdlem103  47312  fourierdlem104  47313  sqwvfoura  47331  sqwvfourb  47332  etransclem15  47352  etransclem24  47361  etransclem25  47362  etransclem32  47369  etransclem35  47372  etransclem48  47385  hoidmvlelem1  47698  hoidmvlelem2  47699  hoidmvlelem3  47700  sharhght  47968  altgsumbcALT  49558  dig0  49811  itcovalpclem1  49875  line2ylem  49956  line2xlem  49958  2itscp  49986