Theorem mul01d 11510

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7421  ℂcc 11199  0cc0 11201   · cmul 11206

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7752  ax-resscn 11258  ax-1cn 11259  ax-icn 11260  ax-addcl 11261  ax-addrcl 11262  ax-mulcl 11263  ax-mulrcl 11264  ax-mulcom 11265  ax-addass 11266  ax-mulass 11267  ax-distr 11268  ax-i2m1 11269  ax-1ne0 11270  ax-1rid 11271  ax-rnegex 11272  ax-rrecex 11273  ax-cnre 11274  ax-pre-lttri 11275  ax-pre-lttrn 11276  ax-pre-ltadd 11277

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3900  df-un 3902  df-in 3904  df-ss 3915  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-er 8718  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11346  df-mnf 11347  df-ltxr 11349

This theorem is used by:  mulge0  11835  mul0or  11957  diveq0  11985  lemul1a  12172  un0mulcl  12641  mul2lt0bi  13229  rexmul  13402  modid  14037  addmodlteq  14090  expmul  14251  sqlecan  14354  discr  14385  hashf1lem2  14602  hashf1  14603  sgnmul  15261  fsummulc2  15951  pwdif  16038  geolim  16040  geomulcvg  16046  fprodeq0  16143  0risefac  16205  0dvds  16447  smumullem  16663  bezoutlem1  16713  lcmgcd  16783  mulgcddvds  16831  cncongr2  16844  prmdiv  16963  pcaddlem  17067  qexpz  17080  prmreclem4  17098  prmreclem5  17099  mulgnn0ass  19321  odadd2  20064  isabvd  21070  nn0srg  21744  rge0srg  21745  pzriprnglem8  21795  mhppwdeg  22472  nmolb2d  25038  nmoleub  25051  reparphti  25319  pcorevlem  25348  itg1val2  26006  i1fmullem  26016  itg1addlem4  26021  itg10a  26032  itg1ge0a  26033  itg2const  26062  itg2monolem1  26072  itg0  26101  itgz  26102  iblmulc2  26152  itgmulc2lem1  26153  bddmulibl  26160  dvcnp2  26241  dvcobr  26267  dvlip  26314  dvlipcn  26315  c1lip1  26318  dvlt0  26326  plymullem1  26534  coefv0  26568  coemullem  26570  coemulhi  26574  dgrmulc  26591  dgrcolem2  26594  dvply1  26606  plydivlem3  26617  elqaalem2  26644  elqaalem3  26645  tayl0  26690  dvtaylp  26698  radcnv0  26744  dvradcnv  26749  pserdvlem2  26756  abelthlem2  26760  pilem2  26780  sinmpi  26817  cosmpi  26818  sinppi  26819  cosppi  26820  tanregt0  26868  efsubm  26880  argregt0  26939  argrege0  26940  argimgt0  26941  logtayl  26989  mulcxplem  27013  mulcxp  27014  cxpmul2  27018  pythag  27146  quad2  27168  dcubic  27175  atans2  27260  zetacvg  27343  lgamgulmlem2  27358  mumul  27509  logexprlim  27553  dchrsum2  27596  sumdchr2  27598  lgsdilem  27652  lgsdirnn0  27672  lgsdinn0  27673  lgsquad3  27715  2sqmod  27764  rpvmasumlem  27815  dchrisumlem1  27817  dchrvmasumiflem2  27830  rpvmasum2  27840  dchrisum0re  27841  pntrlog2bndlem4  27908  pntlemf  27933  pntleml  27939  ostth2lem2  27962  ostth3  27966  colinearalg  29489  nmlnoubi  31399  ipasslem2  31435  cdj3lem1  33037  oexpled  33428  constrrtlc2  34366  cos9thpiminplylem1  34415  cos9thpiminplylem2  34416  xrge0iifhom  34570  signsplypnf  35180  signswch  35191  signlem0  35217  itgexpif  35236  circlemeth  35270  knoppndvlem6  37384  knoppndvlem8  37386  knoppndvlem13  37391  ovoliunnfl  38582  voliunnfl  38584  itg2addnclem  38591  iblmulc2nc  38605  itgmulc2nclem1  38606  areacirc  38633  geomcau  38695  bfp  38760  lcmineqlem10  43090  lcmineqlem12  43092  irrapxlem1  43830  pell1qr1  43879  pell1qrgaplem  43881  rmxy0  43931  jm2.18  43996  mpaaeu  44153  relexpmulg  44711  binomcxplemnotnn0  45341  xralrple2  46367  stoweidlem26  47037  stoweidlem37  47048  stirlinglem7  47091  dirkercncflem2  47115  fourierdlem103  47220  fourierdlem104  47221  sqwvfoura  47239  sqwvfourb  47240  etransclem15  47260  etransclem24  47269  etransclem25  47270  etransclem32  47277  etransclem35  47280  etransclem48  47293  hoidmvlelem1  47606  hoidmvlelem2  47607  hoidmvlelem3  47608  sharhght  47876  altgsumbcALT  49466  dig0  49719  itcovalpclem1  49783  line2ylem  49864  line2xlem  49866  2itscp  49894