Theorem mul01d 11319

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011  0cc0 11013   · cmul 11018

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-ltxr 11158

This theorem is referenced by:  mulge0  11642  mul0or  11764  diveq0  11793  div0OLD  11817  lemul1a  11982  un0mulcl  12422  mul2lt0bi  13000  rexmul  13172  modid  13802  addmodlteq  13855  expmul  14016  sqlecan  14118  discr  14149  hashf1lem2  14365  hashf1  14366  fsummulc2  15693  pwdif  15777  geolim  15779  geomulcvg  15785  fprodeq0  15884  0risefac  15947  0dvds  16189  smumullem  16405  bezoutlem1  16452  lcmgcd  16520  mulgcddvds  16568  cncongr2  16581  prmdiv  16698  pcaddlem  16802  qexpz  16815  prmreclem4  16833  prmreclem5  16834  mulgnn0ass  19025  odadd2  19763  isabvd  20729  nn0srg  21376  rge0srg  21377  pzriprnglem8  21427  mhppwdeg  22066  nmolb2d  24634  nmoleub  24647  reparphti  24924  reparphtiOLD  24925  pcorevlem  24954  itg1val2  25613  i1fmullem  25623  itg1addlem4  25628  itg10a  25639  itg1ge0a  25640  itg2const  25669  itg2monolem1  25679  itg0  25709  itgz  25710  iblmulc2  25760  itgmulc2lem1  25761  bddmulibl  25768  dvcnp2  25849  dvcnp2OLD  25850  dvcobr  25877  dvcobrOLD  25878  dvlip  25926  dvlipcn  25927  c1lip1  25930  dvlt0  25938  plymullem1  26147  coefv0  26181  coemullem  26183  coemulhi  26187  dgrmulc  26205  dgrcolem2  26208  dvply1  26219  plydivlem3  26231  elqaalem2  26256  elqaalem3  26257  tayl0  26297  dvtaylp  26306  radcnv0  26353  dvradcnv  26358  pserdvlem2  26366  abelthlem2  26370  pilem2  26390  sinmpi  26424  cosmpi  26425  sinppi  26426  cosppi  26427  tanregt0  26476  efsubm  26488  argregt0  26547  argrege0  26548  argimgt0  26549  logtayl  26597  mulcxplem  26621  mulcxp  26622  cxpmul2  26626  pythag  26755  quad2  26777  dcubic  26784  atans2  26869  zetacvg  26953  lgamgulmlem2  26968  mumul  27119  logexprlim  27164  dchrsum2  27207  sumdchr2  27209  lgsdilem  27263  lgsdirnn0  27283  lgsdinn0  27284  lgsquad3  27326  2sqmod  27375  rpvmasumlem  27426  dchrisumlem1  27428  dchrvmasumiflem2  27441  rpvmasum2  27451  dchrisum0re  27452  pntrlog2bndlem4  27519  pntlemf  27544  pntleml  27550  ostth2lem2  27573  ostth3  27577  colinearalg  28890  nmlnoubi  30778  ipasslem2  30814  cdj3lem1  32416  sgnmul  32823  oexpled  32835  constrrtlc2  33767  cos9thpiminplylem1  33816  cos9thpiminplylem2  33817  xrge0iifhom  33971  signsplypnf  34584  signswch  34595  signlem0  34621  itgexpif  34640  circlemeth  34674  knoppndvlem6  36582  knoppndvlem8  36584  knoppndvlem13  36589  ovoliunnfl  37722  voliunnfl  37724  itg2addnclem  37731  iblmulc2nc  37745  itgmulc2nclem1  37746  areacirc  37773  geomcau  37819  bfp  37884  lcmineqlem10  42151  lcmineqlem12  42153  irrapxlem1  42939  pell1qr1  42988  pell1qrgaplem  42990  rmxy0  43040  jm2.18  43105  mpaaeu  43267  relexpmulg  43827  binomcxplemnotnn0  44473  xralrple2  45477  stoweidlem26  46148  stoweidlem37  46159  stirlinglem7  46202  dirkercncflem2  46226  fourierdlem103  46331  fourierdlem104  46332  sqwvfoura  46350  sqwvfourb  46351  etransclem15  46371  etransclem24  46380  etransclem25  46381  etransclem32  46388  etransclem35  46391  etransclem48  46404  hoidmvlelem1  46717  hoidmvlelem2  46718  hoidmvlelem3  46719  sharhght  46987  altgsumbcALT  48477  dig0  48731  itcovalpclem1  48795  line2ylem  48876  line2xlem  48878  2itscp  48906