Theorem mul01d 11427

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116  0cc0 11118   · cmul 11123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-po 5574  df-so 5575  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-ltxr 11266

This theorem is used by:  mulge0  11750  mul0or  11872  diveq0  11900  lemul1a  12087  un0mulcl  12556  mul2lt0bi  13142  rexmul  13315  modid  13949  addmodlteq  14002  expmul  14163  sqlecan  14265  discr  14296  hashf1lem2  14513  hashf1  14514  sgnmul  15170  fsummulc2  15861  pwdif  15948  geolim  15950  geomulcvg  15956  fprodeq0  16055  0risefac  16117  0dvds  16359  smumullem  16575  bezoutlem1  16622  lcmgcd  16690  mulgcddvds  16738  cncongr2  16751  prmdiv  16869  pcaddlem  16973  qexpz  16986  prmreclem4  17004  prmreclem5  17005  mulgnn0ass  19207  odadd2  19950  isabvd  20952  nn0srg  21624  rge0srg  21625  pzriprnglem8  21675  mhppwdeg  22350  nmolb2d  24912  nmoleub  24925  reparphti  25193  pcorevlem  25222  itg1val2  25880  i1fmullem  25890  itg1addlem4  25895  itg10a  25906  itg1ge0a  25907  itg2const  25936  itg2monolem1  25946  itg0  25976  itgz  25977  iblmulc2  26027  itgmulc2lem1  26028  bddmulibl  26035  dvcnp2  26116  dvcobr  26142  dvlip  26189  dvlipcn  26190  c1lip1  26193  dvlt0  26201  plymullem1  26408  coefv0  26442  coemullem  26444  coemulhi  26448  dgrmulc  26465  dgrcolem2  26468  dvply1  26482  plydivlem3  26493  elqaalem2  26518  elqaalem3  26519  tayl0  26562  dvtaylp  26570  radcnv0  26616  dvradcnv  26621  pserdvlem2  26628  abelthlem2  26632  pilem2  26652  sinmpi  26689  cosmpi  26690  sinppi  26691  cosppi  26692  tanregt0  26741  efsubm  26753  argregt0  26812  argrege0  26813  argimgt0  26814  logtayl  26862  mulcxplem  26886  mulcxp  26887  cxpmul2  26891  pythag  27019  quad2  27041  dcubic  27048  atans2  27133  zetacvg  27216  lgamgulmlem2  27231  mumul  27382  logexprlim  27426  dchrsum2  27469  sumdchr2  27471  lgsdilem  27525  lgsdirnn0  27545  lgsdinn0  27546  lgsquad3  27588  2sqmod  27637  rpvmasumlem  27688  dchrisumlem1  27690  dchrvmasumiflem2  27703  rpvmasum2  27713  dchrisum0re  27714  pntrlog2bndlem4  27781  pntlemf  27806  pntleml  27812  ostth2lem2  27835  ostth3  27839  colinearalg  29297  nmlnoubi  31185  ipasslem2  31221  cdj3lem1  32823  oexpled  33217  constrrtlc2  34154  cos9thpiminplylem1  34203  cos9thpiminplylem2  34204  xrge0iifhom  34358  signsplypnf  34968  signswch  34979  signlem0  35005  itgexpif  35024  circlemeth  35058  knoppndvlem6  37146  knoppndvlem8  37148  knoppndvlem13  37153  ovoliunnfl  38353  voliunnfl  38355  itg2addnclem  38362  iblmulc2nc  38376  itgmulc2nclem1  38377  areacirc  38404  geomcau  38450  bfp  38515  lcmineqlem10  42845  lcmineqlem12  42847  irrapxlem1  43589  pell1qr1  43638  pell1qrgaplem  43640  rmxy0  43690  jm2.18  43755  mpaaeu  43917  relexpmulg  44476  binomcxplemnotnn0  45106  xralrple2  46110  stoweidlem26  46780  stoweidlem37  46791  stirlinglem7  46834  dirkercncflem2  46858  fourierdlem103  46963  fourierdlem104  46964  sqwvfoura  46982  sqwvfourb  46983  etransclem15  47003  etransclem24  47012  etransclem25  47013  etransclem32  47020  etransclem35  47023  etransclem48  47036  hoidmvlelem1  47349  hoidmvlelem2  47350  hoidmvlelem3  47351  sharhght  47619  altgsumbcALT  49173  dig0  49426  itcovalpclem1  49490  line2ylem  49571  line2xlem  49573  2itscp  49601