Theorem mul02d 11308

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
mul02d	⊢ (𝜑 → (0 · 𝐴) = 0)

Proof of Theorem mul02d

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		mul02 11288	. 2 ⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
3	1, 2	syl 17	1 ⊢ (𝜑 → (0 · 𝐴) = 0)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001  0cc0 11003   · cmul 11008

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-resscn 11060  ax-1cn 11061  ax-icn 11062  ax-addcl 11063  ax-addrcl 11064  ax-mulcl 11065  ax-mulrcl 11066  ax-mulcom 11067  ax-addass 11068  ax-mulass 11069  ax-distr 11070  ax-i2m1 11071  ax-1ne0 11072  ax-1rid 11073  ax-rnegex 11074  ax-rrecex 11075  ax-cnre 11076  ax-pre-lttri 11077  ax-pre-lttrn 11078  ax-pre-ltadd 11079

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-po 5524  df-so 5525  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11145  df-mnf 11146  df-ltxr 11148

This theorem is referenced by:  mulneg1  11550  mulge0  11632  mul0or  11754  prodgt0  11965  un0mulcl  12412  mul2lt0rgt0  12992  mul2lt0bi  12995  lincmb01cmp  13392  iccf1o  13393  discr1  14143  discr  14144  hashxplem  14337  cshweqrep  14725  remul2  15034  immul2  15041  binomlem  15733  geomulcvg  15780  ntrivcvgfvn0  15803  fprodeq0  15879  fprodeq0g  15898  0fallfac  15941  binomfallfaclem2  15944  efne0d  16001  efne0OLD  16003  dvds0  16179  pwp1fsum  16299  smumullem  16400  mulgcd  16456  bezoutr1  16477  lcmgcd  16515  qnumgt0  16658  pcexp  16768  vdwapun  16883  vdwlem1  16890  mulgnn0ass  19020  odmulg  19466  torsubg  19764  isabvd  20725  nn0srg  21372  rge0srg  21373  prmirredlem  21407  pzriprnglem8  21423  nmo0  24648  nmoeq0  24649  blcvx  24711  reparphti  24921  reparphtiOLD  24922  pcorevlem  24951  ipcau2  25159  rrxcph  25317  itg1addlem4  25625  itg1addlem5  25626  itg1mulc  25630  itg2mulc  25673  dvcmul  25872  dvmptcmul  25893  dvexp3  25907  dvef  25909  dveq0  25930  dv11cn  25931  ply1termlem  26133  plyeq0lem  26140  plypf1  26142  plyaddlem1  26143  plymullem1  26144  coeeulem  26154  coeidlem  26167  coeid3  26170  coemullem  26180  coemulhi  26184  coemulc  26185  dgrco  26206  vieta1lem2  26244  elqaalem2  26253  aalioulem3  26267  taylthlem2  26307  taylthlem2OLD  26308  abelthlem6  26371  pilem2  26387  sinhalfpip  26426  sinhalfpim  26427  coshalfpip  26428  coshalfpim  26429  logtayl  26594  mulcxp  26619  cxpmul2  26623  cxpeq  26692  chordthmlem5  26771  cubic  26784  atans2  26866  atantayl2  26873  leibpi  26877  efrlim  26904  efrlimOLD  26905  scvxcvx  26921  amgm  26926  ftalem5  27012  basellem2  27017  mumul  27116  muinv  27128  dchrn0  27186  dchrinvcl  27189  lgsdirnn0  27280  lgsdinn0  27281  lgsquad2lem2  27321  rpvmasumlem  27423  dchrisum0flblem1  27444  rpvmasum2  27448  ostth2lem2  27570  brbtwn2  28881  axsegconlem1  28893  axpaschlem  28916  axcontlem7  28946  axcontlem8  28947  elntg2  28961  nvz0  30643  ipasslem1  30806  hi01  31071  fprodeq02  32801  sgnmul  32813  indsum  32837  indsumin  32838  constrrtcc  33743  constrsslem  33749  constrremulcl  33775  2sqr3minply  33788  cos9thpiminplylem2  33791  xrge0iifhom  33945  eulerpartlemsv2  34366  eulerpartlems  34368  eulerpartlemsv3  34369  eulerpartlemgc  34370  eulerpartlemv  34372  eulerpartlemgs2  34388  plymul02  34554  plymulx0  34555  itgexpif  34614  breprexplemc  34640  breprexp  34641  logdivsqrle  34658  subfacp1lem6  35217  cvxpconn  35274  cvxsconn  35275  fwddifnp1  36198  lcmineqlem10  42070  deg1pow  42173  pell1234qrne0  42885  jm2.19lem3  43023  jm2.25  43031  flcidc  43202  relexpmulg  43742  radcnvrat  44346  dvconstbi  44366  binomcxplemnn0  44381  sineq0ALT  44968  fperiodmullem  45343  fprod0  45635  dvsinax  45950  dvasinbx  45957  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvnxpaek  45979  dvnmul  45980  itgsinexplem1  45991  dirkertrigeqlem2  46136  fourierdlem42  46186  fourierdlem83  46226  sqwvfoura  46265  fouriersw  46268  elaa2lem  46270  etransclem15  46286  etransclem24  46295  etransclem35  46306  etransclem46  46317  sigarcol  46901  sharhght  46902  modlt0b  47393  fmtnofac2  47599  rrx2linest  48773  line2x  48785  line2y  48786  itschlc0yqe  48791  itschlc0xyqsol1  48797  itschlc0xyqsol  48798  2itscp  48812  aacllem  49832