Theorem mul02d 11374

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  (class class class)co 7390  ℂcc 11064  0cc0 11066   · cmul 11071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-resscn 11123  ax-1cn 11124  ax-icn 11125  ax-addcl 11126  ax-addrcl 11127  ax-mulcl 11128  ax-mulrcl 11129  ax-mulcom 11130  ax-addass 11131  ax-mulass 11132  ax-distr 11133  ax-i2m1 11134  ax-1ne0 11135  ax-1rid 11136  ax-rnegex 11137  ax-rrecex 11138  ax-cnre 11139  ax-pre-lttri 11140  ax-pre-lttrn 11141  ax-pre-ltadd 11142

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-er 8671  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-ltxr 11214

This theorem is referenced by:  mulneg1  11616  mulge0  11698  mul0or  11820  prodgt0  12031  un0mulcl  12508  mul2lt0rgt0  13091  mul2lt0bi  13094  lincmb01cmp  13492  iccf1o  13493  discr1  14245  discr  14246  hashxplem  14439  cshweqrep  14827  sgnmul  15110  remul2  15147  immul2  15154  indsum  15846  binomlem  15849  geomulcvg  15896  ntrivcvgfvn0  15919  fprodeq0  15995  fprodeq0g  16014  0fallfac  16057  binomfallfaclem2  16060  efne0d  16117  efne0OLD  16119  dvds0  16295  pwp1fsum  16415  smumullem  16516  mulgcd  16572  bezoutr1  16593  lcmgcd  16631  qnumgt0  16775  pcexp  16885  vdwapun  17000  vdwlem1  17007  mulgnn0ass  19142  odmulg  19586  torsubg  19884  isabvd  20848  nn0srg  21476  rge0srg  21477  prmirredlem  21511  pzriprnglem8  21527  nmo0  24782  nmoeq0  24783  blcvx  24845  reparphti  25046  pcorevlem  25075  ipcau2  25283  rrxcph  25441  itg1addlem4  25748  itg1addlem5  25749  itg1mulc  25753  itg2mulc  25796  dvcmul  25993  dvmptcmul  26013  dvexp3  26027  dvef  26029  dveq0  26049  dv11cn  26050  ply1termlem  26250  plyeq0lem  26257  plypf1  26259  plyaddlem1  26260  plymullem1  26261  coeeulem  26271  coeidlem  26284  coeid3  26287  coemullem  26297  coemulhi  26301  coemulc  26302  dgrco  26322  plymul02  26331  plyn0mulidp  26332  vieta1lem2  26362  elqaalem2  26371  aalioulem3  26385  taylthlem2  26424  abelthlem6  26486  pilem2  26502  sinhalfpip  26544  sinhalfpim  26545  coshalfpip  26546  coshalfpim  26547  logtayl  26712  mulcxp  26737  cxpmul2  26741  cxpeq  26809  chordthmlem5  26888  cubic  26901  atans2  26983  atantayl2  26990  leibpi  26994  efrlim  27021  scvxcvx  27037  amgm  27042  ftalem5  27128  basellem2  27133  mumul  27232  muinv  27244  dchrn0  27301  dchrinvcl  27304  lgsdirnn0  27395  lgsdinn0  27396  lgsquad2lem2  27436  rpvmasumlem  27538  dchrisum0flblem1  27559  rpvmasum2  27563  ostth2lem2  27685  brbtwn2  29062  axsegconlem1  29074  axpaschlem  29097  axcontlem7  29127  axcontlem8  29128  elntg2  29142  nvz0  30827  ipasslem1  30990  hi01  31255  fprodeq02  32986  indsumin  32999  constrrtcc  33992  constrsslem  33998  constrremulcl  34024  2sqr3minply  34037  cos9thpiminplylem2  34040  xrge0iifhom  34194  eulerpartlemsv2  34615  eulerpartlems  34617  eulerpartlemsv3  34618  eulerpartlemgc  34619  eulerpartlemv  34621  eulerpartlemgs2  34637  itgexpif  34860  breprexplemc  34886  breprexp  34887  logdivsqrle  34904  subfacp1lem6  35495  cvxpconn  35552  cvxsconn  35553  fwddifnp1  36475  lcmineqlem10  42615  deg1pow  42718  pell1234qrne0  43390  jm2.19lem3  43528  jm2.25  43536  flcidc  43707  relexpmulg  44246  radcnvrat  44850  dvconstbi  44870  binomcxplemnn0  44885  sineq0ALT  45472  fperiodmullem  45842  fprod0  46132  dvsinax  46447  dvasinbx  46454  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  dvnxpaek  46476  dvnmul  46477  itgsinexplem1  46488  dirkertrigeqlem2  46633  fourierdlem42  46683  fourierdlem83  46723  sqwvfoura  46762  fouriersw  46765  elaa2lem  46767  etransclem15  46783  etransclem24  46792  etransclem35  46803  etransclem46  46814  sigarcol  47398  sharhght  47399  modlt0b  47923  fmtnofac2  48138  rrx2linest  49324  line2x  49336  line2y  49337  itschlc0yqe  49342  itschlc0xyqsol1  49348  itschlc0xyqsol  49349  2itscp  49363  aacllem  50382