Theorem mul01d 10841

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537  0cc0 10539   · cmul 10544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-po 5476  df-so 5477  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-ltxr 10682

This theorem is referenced by:  mulge0  11160  mul0or  11282  diveq0  11310  div0  11330  lemul1a  11496  un0mulcl  11934  mul2lt0bi  12498  rexmul  12667  modid  13267  addmodlteq  13317  expmul  13477  sqlecan  13574  discr  13604  hashf1lem2  13817  hashf1  13818  fsummulc2  15141  pwdif  15225  geolim  15228  geomulcvg  15234  fprodeq0  15331  0risefac  15394  0dvds  15632  smumullem  15843  bezoutlem1  15889  lcmgcd  15953  mulgcddvds  16001  cncongr2  16014  prmdiv  16124  pcaddlem  16226  qexpz  16239  prmreclem4  16257  prmreclem5  16258  mulgnn0ass  18265  odadd2  18971  isabvd  19593  nn0srg  20617  rge0srg  20618  nmolb2d  23329  nmoleub  23342  reparphti  23603  pcorevlem  23632  itg1val2  24287  i1fmullem  24297  itg1addlem4  24302  itg10a  24313  itg1ge0a  24314  itg2const  24343  itg2monolem1  24353  itg0  24382  itgz  24383  iblmulc2  24433  itgmulc2lem1  24434  bddmulibl  24441  dvcnp2  24519  dvcobr  24545  dvlip  24592  dvlipcn  24593  c1lip1  24596  dvlt0  24604  plymullem1  24806  coefv0  24840  coemullem  24842  coemulhi  24846  dgrmulc  24863  dgrcolem2  24866  dvply1  24875  plydivlem3  24886  elqaalem2  24911  elqaalem3  24912  tayl0  24952  dvtaylp  24960  radcnv0  25006  dvradcnv  25011  pserdvlem2  25018  abelthlem2  25022  pilem2  25042  sinmpi  25075  cosmpi  25076  sinppi  25077  cosppi  25078  tanregt0  25125  efsubm  25137  argregt0  25195  argrege0  25196  argimgt0  25197  logtayl  25245  mulcxplem  25269  mulcxp  25270  cxpmul2  25274  pythag  25397  quad2  25419  dcubic  25426  atans2  25511  zetacvg  25594  lgamgulmlem2  25609  mumul  25760  logexprlim  25803  dchrsum2  25846  sumdchr2  25848  lgsdilem  25902  lgsdirnn0  25922  lgsdinn0  25923  lgsquad3  25965  2sqmod  26014  rpvmasumlem  26065  dchrisumlem1  26067  dchrvmasumiflem2  26080  rpvmasum2  26090  dchrisum0re  26091  pntrlog2bndlem4  26158  pntlemf  26183  pntleml  26189  ostth2lem2  26212  ostth3  26216  colinearalg  26698  nmlnoubi  28575  ipasslem2  28611  cdj3lem1  30213  xrge0iifhom  31182  sgnmul  31802  signsplypnf  31822  signswch  31833  signlem0  31859  itgexpif  31879  circlemeth  31913  knoppndvlem6  33858  knoppndvlem8  33860  knoppndvlem13  33865  ovoliunnfl  34936  voliunnfl  34938  itg2addnclem  34945  iblmulc2nc  34959  itgmulc2nclem1  34960  areacirc  34989  geomcau  35036  bfp  35104  irrapxlem1  39426  pell1qr1  39475  pell1qrgaplem  39477  rmxy0  39527  jm2.18  39592  mpaaeu  39757  relexpmulg  40062  binomcxplemnotnn0  40695  xralrple2  41629  stoweidlem26  42318  stoweidlem37  42329  stirlinglem7  42372  dirkercncflem2  42396  fourierdlem103  42501  fourierdlem104  42502  sqwvfoura  42520  sqwvfourb  42521  etransclem15  42541  etransclem24  42550  etransclem25  42551  etransclem32  42558  etransclem35  42561  etransclem48  42574  hoidmvlelem1  42884  hoidmvlelem2  42885  hoidmvlelem3  42886  sharhght  43129  altgsumbcALT  44408  dig0  44673  line2ylem  44745  line2xlem  44747  2itscp  44775