Theorem mul01d 10639

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

Syntax hints:   → wi 4   = wceq 1507   ∈ wcel 2050  (class class class)co 6976  ℂcc 10333  0cc0 10335   · cmul 10340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-po 5326  df-so 5327  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-ov 6979  df-er 8089  df-en 8307  df-dom 8308  df-sdom 8309  df-pnf 10476  df-mnf 10477  df-ltxr 10479

This theorem is referenced by:  mulge0  10959  mul0or  11081  diveq0  11109  div0  11129  lemul1a  11295  un0mulcl  11743  mul2lt0bi  12312  rexmul  12480  modid  13079  addmodlteq  13129  expmul  13289  sqlecan  13386  discr  13416  hashf1lem2  13627  hashf1  13628  fsummulc2  14999  pwdif  15083  geolim  15086  geomulcvg  15092  fprodeq0  15189  0risefac  15252  0dvds  15490  smumullem  15701  bezoutlem1  15743  lcmgcd  15807  mulgcddvds  15855  cncongr2  15868  prmdiv  15978  pcaddlem  16080  qexpz  16093  prmreclem4  16111  prmreclem5  16112  mulgnn0ass  18047  odadd2  18725  isabvd  19313  nn0srg  20317  rge0srg  20318  nmolb2d  23030  nmoleub  23043  reparphti  23304  pcorevlem  23333  itg1val2  23988  i1fmullem  23998  itg1addlem4  24003  itg10a  24014  itg1ge0a  24015  itg2const  24044  itg2monolem1  24054  itg0  24083  itgz  24084  iblmulc2  24134  itgmulc2lem1  24135  bddmulibl  24142  dvcnp2  24220  dvcobr  24246  dvlip  24293  dvlipcn  24294  c1lip1  24297  dvlt0  24305  plymullem1  24507  coefv0  24541  coemullem  24543  coemulhi  24547  dgrmulc  24564  dgrcolem2  24567  dvply1  24576  plydivlem3  24587  elqaalem2  24612  elqaalem3  24613  tayl0  24653  dvtaylp  24661  radcnv0  24707  dvradcnv  24712  pserdvlem2  24719  abelthlem2  24723  pilem2  24743  sinmpi  24776  cosmpi  24777  sinppi  24778  cosppi  24779  tanregt0  24824  efsubm  24836  argregt0  24894  argrege0  24895  argimgt0  24896  logtayl  24944  mulcxplem  24968  mulcxp  24969  cxpmul2  24973  pythag  25096  quad2  25118  dcubic  25125  atans2  25210  zetacvg  25294  lgamgulmlem2  25309  mumul  25460  logexprlim  25503  dchrsum2  25546  sumdchr2  25548  lgsdilem  25602  lgsdirnn0  25622  lgsdinn0  25623  lgsquad3  25665  2sqmod  25714  rpvmasumlem  25765  dchrisumlem1  25767  dchrvmasumiflem2  25780  rpvmasum2  25790  dchrisum0re  25791  pntrlog2bndlem4  25858  pntlemf  25883  pntleml  25889  ostth2lem2  25912  ostth3  25916  colinearalg  26399  nmlnoubi  28350  ipasslem2  28386  cdj3lem1  29992  xrge0iifhom  30830  sgnmul  31452  signsplypnf  31472  signswch  31483  signlem0  31511  itgexpif  31531  circlemeth  31565  knoppndvlem6  33382  knoppndvlem8  33384  knoppndvlem13  33389  ovoliunnfl  34381  voliunnfl  34383  itg2addnclem  34390  iblmulc2nc  34404  itgmulc2nclem1  34405  areacirc  34434  geomcau  34482  bfp  34550  irrapxlem1  38821  pell1qr1  38870  pell1qrgaplem  38872  rmxy0  38922  jm2.18  38987  mpaaeu  39152  relexpmulg  39424  binomcxplemnotnn0  40110  xralrple2  41057  stoweidlem26  41748  stoweidlem37  41759  stirlinglem7  41802  dirkercncflem2  41826  fourierdlem103  41931  fourierdlem104  41932  sqwvfoura  41950  sqwvfourb  41951  etransclem15  41971  etransclem24  41980  etransclem25  41981  etransclem32  41988  etransclem35  41991  etransclem48  42004  hoidmvlelem1  42314  hoidmvlelem2  42315  hoidmvlelem3  42316  sharhght  42559  altgsumbcALT  43771  dig0  44040  line2ylem  44112  line2xlem  44114  2itscp  44142