Theorem mul01d 11379

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068  0cc0 11070   · cmul 11075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-resscn 11127  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-addrcl 11131  ax-mulcl 11132  ax-mulrcl 11133  ax-mulcom 11134  ax-addass 11135  ax-mulass 11136  ax-distr 11137  ax-i2m1 11138  ax-1ne0 11139  ax-1rid 11140  ax-rnegex 11141  ax-rrecex 11142  ax-cnre 11143  ax-pre-lttri 11144  ax-pre-lttrn 11145  ax-pre-ltadd 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-po 5553  df-so 5554  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-ov 7395  df-er 8673  df-en 8924  df-dom 8925  df-sdom 8926  df-pnf 11215  df-mnf 11216  df-ltxr 11218

This theorem is referenced by:  mulge0  11702  mul0or  11824  diveq0  11852  div0OLD  11876  lemul1a  12042  un0mulcl  12512  mul2lt0bi  13098  rexmul  13271  modid  13903  addmodlteq  13956  expmul  14117  sqlecan  14219  discr  14250  hashf1lem2  14466  hashf1  14467  fsummulc2  15794  pwdif  15881  geolim  15883  geomulcvg  15889  fprodeq0  15988  0risefac  16051  0dvds  16293  smumullem  16509  bezoutlem1  16556  lcmgcd  16624  mulgcddvds  16672  cncongr2  16685  prmdiv  16803  pcaddlem  16907  qexpz  16920  prmreclem4  16938  prmreclem5  16939  mulgnn0ass  19135  odadd2  19872  isabvd  20841  nn0srg  21469  rge0srg  21470  pzriprnglem8  21520  mhppwdeg  22195  nmolb2d  24758  nmoleub  24771  reparphti  25039  pcorevlem  25068  itg1val2  25726  i1fmullem  25736  itg1addlem4  25741  itg10a  25752  itg1ge0a  25753  itg2const  25782  itg2monolem1  25792  itg0  25822  itgz  25823  iblmulc2  25873  itgmulc2lem1  25874  bddmulibl  25881  dvcnp2  25962  dvcobr  25988  dvlip  26035  dvlipcn  26036  c1lip1  26039  dvlt0  26047  plymullem1  26254  coefv0  26288  coemullem  26290  coemulhi  26294  dgrmulc  26311  dgrcolem2  26314  dvply1  26325  plydivlem3  26336  elqaalem2  26361  elqaalem3  26362  tayl0  26402  dvtaylp  26410  radcnv0  26456  dvradcnv  26461  pserdvlem2  26468  abelthlem2  26472  pilem2  26492  sinmpi  26529  cosmpi  26530  sinppi  26531  cosppi  26532  tanregt0  26581  efsubm  26593  argregt0  26652  argrege0  26653  argimgt0  26654  logtayl  26702  mulcxplem  26726  mulcxp  26727  cxpmul2  26731  pythag  26859  quad2  26881  dcubic  26888  atans2  26973  zetacvg  27056  lgamgulmlem2  27071  mumul  27222  logexprlim  27266  dchrsum2  27309  sumdchr2  27311  lgsdilem  27365  lgsdirnn0  27385  lgsdinn0  27386  lgsquad3  27428  2sqmod  27477  rpvmasumlem  27528  dchrisumlem1  27530  dchrvmasumiflem2  27543  rpvmasum2  27553  dchrisum0re  27554  pntrlog2bndlem4  27621  pntlemf  27646  pntleml  27652  ostth2lem2  27675  ostth3  27679  colinearalg  29057  nmlnoubi  30945  ipasslem2  30981  cdj3lem1  32583  sgnmul  32987  oexpled  32999  constrrtlc2  33991  cos9thpiminplylem1  34040  cos9thpiminplylem2  34041  xrge0iifhom  34195  signsplypnf  34808  signswch  34819  signlem0  34845  itgexpif  34864  circlemeth  34898  knoppndvlem6  36919  knoppndvlem8  36921  knoppndvlem13  36926  ovoliunnfl  38125  voliunnfl  38127  itg2addnclem  38134  iblmulc2nc  38148  itgmulc2nclem1  38149  areacirc  38176  geomcau  38222  bfp  38287  lcmineqlem10  42619  lcmineqlem12  42621  irrapxlem1  43363  pell1qr1  43412  pell1qrgaplem  43414  rmxy0  43464  jm2.18  43529  mpaaeu  43691  relexpmulg  44250  binomcxplemnotnn0  44896  xralrple2  45894  stoweidlem26  46564  stoweidlem37  46575  stirlinglem7  46618  dirkercncflem2  46642  fourierdlem103  46747  fourierdlem104  46748  sqwvfoura  46766  sqwvfourb  46767  etransclem15  46787  etransclem24  46796  etransclem25  46797  etransclem32  46804  etransclem35  46807  etransclem48  46820  hoidmvlelem1  47133  hoidmvlelem2  47134  hoidmvlelem3  47135  sharhght  47403  altgsumbcALT  48939  dig0  49192  itcovalpclem1  49256  line2ylem  49337  line2xlem  49339  2itscp  49367