Theorem mul02d 11331

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  0cc0 11026   · cmul 11031

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171

This theorem is referenced by:  mulneg1  11573  mulge0  11655  mul0or  11777  prodgt0  11988  un0mulcl  12435  mul2lt0rgt0  13010  mul2lt0bi  13013  lincmb01cmp  13411  iccf1o  13412  discr1  14162  discr  14163  hashxplem  14356  cshweqrep  14744  remul2  15053  immul2  15060  binomlem  15752  geomulcvg  15799  ntrivcvgfvn0  15822  fprodeq0  15898  fprodeq0g  15917  0fallfac  15960  binomfallfaclem2  15963  efne0d  16020  efne0OLD  16022  dvds0  16198  pwp1fsum  16318  smumullem  16419  mulgcd  16475  bezoutr1  16496  lcmgcd  16534  qnumgt0  16677  pcexp  16787  vdwapun  16902  vdwlem1  16909  mulgnn0ass  19040  odmulg  19485  torsubg  19783  isabvd  20745  nn0srg  21392  rge0srg  21393  prmirredlem  21427  pzriprnglem8  21443  nmo0  24679  nmoeq0  24680  blcvx  24742  reparphti  24952  reparphtiOLD  24953  pcorevlem  24982  ipcau2  25190  rrxcph  25348  itg1addlem4  25656  itg1addlem5  25657  itg1mulc  25661  itg2mulc  25704  dvcmul  25903  dvmptcmul  25924  dvexp3  25938  dvef  25940  dveq0  25961  dv11cn  25962  ply1termlem  26164  plyeq0lem  26171  plypf1  26173  plyaddlem1  26174  plymullem1  26175  coeeulem  26185  coeidlem  26198  coeid3  26201  coemullem  26211  coemulhi  26215  coemulc  26216  dgrco  26237  vieta1lem2  26275  elqaalem2  26284  aalioulem3  26298  taylthlem2  26338  taylthlem2OLD  26339  abelthlem6  26402  pilem2  26418  sinhalfpip  26457  sinhalfpim  26458  coshalfpip  26459  coshalfpim  26460  logtayl  26625  mulcxp  26650  cxpmul2  26654  cxpeq  26723  chordthmlem5  26802  cubic  26815  atans2  26897  atantayl2  26904  leibpi  26908  efrlim  26935  efrlimOLD  26936  scvxcvx  26952  amgm  26957  ftalem5  27043  basellem2  27048  mumul  27147  muinv  27159  dchrn0  27217  dchrinvcl  27220  lgsdirnn0  27311  lgsdinn0  27312  lgsquad2lem2  27352  rpvmasumlem  27454  dchrisum0flblem1  27475  rpvmasum2  27479  ostth2lem2  27601  brbtwn2  28978  axsegconlem1  28990  axpaschlem  29013  axcontlem7  29043  axcontlem8  29044  elntg2  29058  nvz0  30743  ipasslem1  30906  hi01  31171  fprodeq02  32904  sgnmul  32916  indsum  32942  indsumin  32943  constrrtcc  33892  constrsslem  33898  constrremulcl  33924  2sqr3minply  33937  cos9thpiminplylem2  33940  xrge0iifhom  34094  eulerpartlemsv2  34515  eulerpartlems  34517  eulerpartlemsv3  34518  eulerpartlemgc  34519  eulerpartlemv  34521  eulerpartlemgs2  34537  plymul02  34703  plymulx0  34704  itgexpif  34763  breprexplemc  34789  breprexp  34790  logdivsqrle  34807  subfacp1lem6  35379  cvxpconn  35436  cvxsconn  35437  fwddifnp1  36359  lcmineqlem10  42288  deg1pow  42391  pell1234qrne0  43091  jm2.19lem3  43229  jm2.25  43237  flcidc  43408  relexpmulg  43947  radcnvrat  44551  dvconstbi  44571  binomcxplemnn0  44586  sineq0ALT  45173  fperiodmullem  45547  fprod0  45838  dvsinax  46153  dvasinbx  46160  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvnxpaek  46182  dvnmul  46183  itgsinexplem1  46194  dirkertrigeqlem2  46339  fourierdlem42  46389  fourierdlem83  46429  sqwvfoura  46468  fouriersw  46471  elaa2lem  46473  etransclem15  46489  etransclem24  46498  etransclem35  46509  etransclem46  46520  sigarcol  47104  sharhght  47105  modlt0b  47605  fmtnofac2  47811  rrx2linest  48984  line2x  48996  line2y  48997  itschlc0yqe  49002  itschlc0xyqsol1  49008  itschlc0xyqsol  49009  2itscp  49023  aacllem  50042