Theorem mul01d 11434

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127  0cc0 11129   · cmul 11134

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 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-ltxr 11274

This theorem is referenced by:  mulge0  11755  mul0or  11877  diveq0  11906  div0OLD  11930  lemul1a  12095  un0mulcl  12535  mul2lt0bi  13115  rexmul  13287  modid  13913  addmodlteq  13964  expmul  14125  sqlecan  14227  discr  14258  hashf1lem2  14474  hashf1  14475  fsummulc2  15800  pwdif  15884  geolim  15886  geomulcvg  15892  fprodeq0  15991  0risefac  16054  0dvds  16296  smumullem  16511  bezoutlem1  16558  lcmgcd  16626  mulgcddvds  16674  cncongr2  16687  prmdiv  16804  pcaddlem  16908  qexpz  16921  prmreclem4  16939  prmreclem5  16940  mulgnn0ass  19093  odadd2  19830  isabvd  20772  nn0srg  21405  rge0srg  21406  pzriprnglem8  21449  mhppwdeg  22088  nmolb2d  24657  nmoleub  24670  reparphti  24947  reparphtiOLD  24948  pcorevlem  24977  itg1val2  25637  i1fmullem  25647  itg1addlem4  25652  itg10a  25663  itg1ge0a  25664  itg2const  25693  itg2monolem1  25703  itg0  25733  itgz  25734  iblmulc2  25784  itgmulc2lem1  25785  bddmulibl  25792  dvcnp2  25873  dvcnp2OLD  25874  dvcobr  25901  dvcobrOLD  25902  dvlip  25950  dvlipcn  25951  c1lip1  25954  dvlt0  25962  plymullem1  26171  coefv0  26205  coemullem  26207  coemulhi  26211  dgrmulc  26229  dgrcolem2  26232  dvply1  26243  plydivlem3  26255  elqaalem2  26280  elqaalem3  26281  tayl0  26321  dvtaylp  26330  radcnv0  26377  dvradcnv  26382  pserdvlem2  26390  abelthlem2  26394  pilem2  26414  sinmpi  26448  cosmpi  26449  sinppi  26450  cosppi  26451  tanregt0  26500  efsubm  26512  argregt0  26571  argrege0  26572  argimgt0  26573  logtayl  26621  mulcxplem  26645  mulcxp  26646  cxpmul2  26650  pythag  26779  quad2  26801  dcubic  26808  atans2  26893  zetacvg  26977  lgamgulmlem2  26992  mumul  27143  logexprlim  27188  dchrsum2  27231  sumdchr2  27233  lgsdilem  27287  lgsdirnn0  27307  lgsdinn0  27308  lgsquad3  27350  2sqmod  27399  rpvmasumlem  27450  dchrisumlem1  27452  dchrvmasumiflem2  27465  rpvmasum2  27475  dchrisum0re  27476  pntrlog2bndlem4  27543  pntlemf  27568  pntleml  27574  ostth2lem2  27597  ostth3  27601  colinearalg  28889  nmlnoubi  30777  ipasslem2  30813  cdj3lem1  32415  sgnmul  32814  oexpled  32826  constrrtlc2  33767  cos9thpiminplylem1  33816  cos9thpiminplylem2  33817  xrge0iifhom  33968  signsplypnf  34582  signswch  34593  signlem0  34619  itgexpif  34638  circlemeth  34672  knoppndvlem6  36535  knoppndvlem8  36537  knoppndvlem13  36542  ovoliunnfl  37686  voliunnfl  37688  itg2addnclem  37695  iblmulc2nc  37709  itgmulc2nclem1  37710  areacirc  37737  geomcau  37783  bfp  37848  lcmineqlem10  42051  lcmineqlem12  42053  irrapxlem1  42845  pell1qr1  42894  pell1qrgaplem  42896  rmxy0  42947  jm2.18  43012  mpaaeu  43174  relexpmulg  43734  binomcxplemnotnn0  44380  xralrple2  45381  stoweidlem26  46055  stoweidlem37  46066  stirlinglem7  46109  dirkercncflem2  46133  fourierdlem103  46238  fourierdlem104  46239  sqwvfoura  46257  sqwvfourb  46258  etransclem15  46278  etransclem24  46287  etransclem25  46288  etransclem32  46295  etransclem35  46298  etransclem48  46311  hoidmvlelem1  46624  hoidmvlelem2  46625  hoidmvlelem3  46626  sharhght  46894  altgsumbcALT  48328  dig0  48586  itcovalpclem1  48650  line2ylem  48731  line2xlem  48733  2itscp  48761