Theorem mul01d 10832

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2113  (class class class)co 7149  ℂcc 10528  0cc0 10530   · cmul 10535

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5323  ax-un 7454  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-nel 3123  df-ral 3142  df-rex 3143  df-rab 3146  df-v 3493  df-sbc 3769  df-csb 3877  df-dif 3932  df-un 3934  df-in 3936  df-ss 3945  df-nul 4285  df-if 4461  df-pw 4534  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7152  df-er 8282  df-en 8503  df-dom 8504  df-sdom 8505  df-pnf 10670  df-mnf 10671  df-ltxr 10673

This theorem is referenced by:  mulge0  11151  mul0or  11273  diveq0  11301  div0  11321  lemul1a  11487  un0mulcl  11925  mul2lt0bi  12489  rexmul  12658  modid  13261  addmodlteq  13311  expmul  13471  sqlecan  13568  discr  13598  hashf1lem2  13811  hashf1  13812  fsummulc2  15134  pwdif  15218  geolim  15221  geomulcvg  15227  fprodeq0  15324  0risefac  15387  0dvds  15625  smumullem  15836  bezoutlem1  15882  lcmgcd  15946  mulgcddvds  15994  cncongr2  16007  prmdiv  16117  pcaddlem  16219  qexpz  16232  prmreclem4  16250  prmreclem5  16251  mulgnn0ass  18258  odadd2  18964  isabvd  19586  nn0srg  20610  rge0srg  20611  nmolb2d  23322  nmoleub  23335  reparphti  23596  pcorevlem  23625  itg1val2  24280  i1fmullem  24290  itg1addlem4  24295  itg10a  24306  itg1ge0a  24307  itg2const  24336  itg2monolem1  24346  itg0  24375  itgz  24376  iblmulc2  24426  itgmulc2lem1  24427  bddmulibl  24434  dvcnp2  24514  dvcobr  24540  dvlip  24587  dvlipcn  24588  c1lip1  24591  dvlt0  24599  plymullem1  24802  coefv0  24836  coemullem  24838  coemulhi  24842  dgrmulc  24859  dgrcolem2  24862  dvply1  24871  plydivlem3  24882  elqaalem2  24907  elqaalem3  24908  tayl0  24948  dvtaylp  24956  radcnv0  25002  dvradcnv  25007  pserdvlem2  25014  abelthlem2  25018  pilem2  25038  sinmpi  25071  cosmpi  25072  sinppi  25073  cosppi  25074  tanregt0  25121  efsubm  25133  argregt0  25191  argrege0  25192  argimgt0  25193  logtayl  25241  mulcxplem  25265  mulcxp  25266  cxpmul2  25270  pythag  25393  quad2  25415  dcubic  25422  atans2  25507  zetacvg  25590  lgamgulmlem2  25605  mumul  25756  logexprlim  25799  dchrsum2  25842  sumdchr2  25844  lgsdilem  25898  lgsdirnn0  25918  lgsdinn0  25919  lgsquad3  25961  2sqmod  26010  rpvmasumlem  26061  dchrisumlem1  26063  dchrvmasumiflem2  26076  rpvmasum2  26086  dchrisum0re  26087  pntrlog2bndlem4  26154  pntlemf  26179  pntleml  26185  ostth2lem2  26208  ostth3  26212  colinearalg  26694  nmlnoubi  28571  ipasslem2  28607  cdj3lem1  30209  xrge0iifhom  31201  sgnmul  31821  signsplypnf  31841  signswch  31852  signlem0  31878  itgexpif  31898  circlemeth  31932  knoppndvlem6  33877  knoppndvlem8  33879  knoppndvlem13  33884  ovoliunnfl  34969  voliunnfl  34971  itg2addnclem  34978  iblmulc2nc  34992  itgmulc2nclem1  34993  areacirc  35020  geomcau  35067  bfp  35135  irrapxlem1  39495  pell1qr1  39544  pell1qrgaplem  39546  rmxy0  39596  jm2.18  39661  mpaaeu  39826  relexpmulg  40129  binomcxplemnotnn0  40762  xralrple2  41696  stoweidlem26  42385  stoweidlem37  42396  stirlinglem7  42439  dirkercncflem2  42463  fourierdlem103  42568  fourierdlem104  42569  sqwvfoura  42587  sqwvfourb  42588  etransclem15  42608  etransclem24  42617  etransclem25  42618  etransclem32  42625  etransclem35  42628  etransclem48  42641  hoidmvlelem1  42951  hoidmvlelem2  42952  hoidmvlelem3  42953  sharhght  43196  altgsumbcALT  44475  dig0  44740  line2ylem  44812  line2xlem  44814  2itscp  44842