Theorem mul02d 11343

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  0cc0 11038   · cmul 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183

This theorem is referenced by:  mulneg1  11585  mulge0  11667  mul0or  11789  prodgt0  12000  un0mulcl  12447  mul2lt0rgt0  13022  mul2lt0bi  13025  lincmb01cmp  13423  iccf1o  13424  discr1  14174  discr  14175  hashxplem  14368  cshweqrep  14756  remul2  15065  immul2  15072  binomlem  15764  geomulcvg  15811  ntrivcvgfvn0  15834  fprodeq0  15910  fprodeq0g  15929  0fallfac  15972  binomfallfaclem2  15975  efne0d  16032  efne0OLD  16034  dvds0  16210  pwp1fsum  16330  smumullem  16431  mulgcd  16487  bezoutr1  16508  lcmgcd  16546  qnumgt0  16689  pcexp  16799  vdwapun  16914  vdwlem1  16921  mulgnn0ass  19052  odmulg  19497  torsubg  19795  isabvd  20757  nn0srg  21404  rge0srg  21405  prmirredlem  21439  pzriprnglem8  21455  nmo0  24691  nmoeq0  24692  blcvx  24754  reparphti  24964  reparphtiOLD  24965  pcorevlem  24994  ipcau2  25202  rrxcph  25360  itg1addlem4  25668  itg1addlem5  25669  itg1mulc  25673  itg2mulc  25716  dvcmul  25915  dvmptcmul  25936  dvexp3  25950  dvef  25952  dveq0  25973  dv11cn  25974  ply1termlem  26176  plyeq0lem  26183  plypf1  26185  plyaddlem1  26186  plymullem1  26187  coeeulem  26197  coeidlem  26210  coeid3  26213  coemullem  26223  coemulhi  26227  coemulc  26228  dgrco  26249  vieta1lem2  26287  elqaalem2  26296  aalioulem3  26310  taylthlem2  26350  taylthlem2OLD  26351  abelthlem6  26414  pilem2  26430  sinhalfpip  26469  sinhalfpim  26470  coshalfpip  26471  coshalfpim  26472  logtayl  26637  mulcxp  26662  cxpmul2  26666  cxpeq  26735  chordthmlem5  26814  cubic  26827  atans2  26909  atantayl2  26916  leibpi  26920  efrlim  26947  efrlimOLD  26948  scvxcvx  26964  amgm  26969  ftalem5  27055  basellem2  27060  mumul  27159  muinv  27171  dchrn0  27229  dchrinvcl  27232  lgsdirnn0  27323  lgsdinn0  27324  lgsquad2lem2  27364  rpvmasumlem  27466  dchrisum0flblem1  27487  rpvmasum2  27491  ostth2lem2  27613  brbtwn2  28990  axsegconlem1  29002  axpaschlem  29025  axcontlem7  29055  axcontlem8  29056  elntg2  29070  nvz0  30755  ipasslem1  30918  hi01  31183  fprodeq02  32914  sgnmul  32926  indsum  32952  indsumin  32953  constrrtcc  33912  constrsslem  33918  constrremulcl  33944  2sqr3minply  33957  cos9thpiminplylem2  33960  xrge0iifhom  34114  eulerpartlemsv2  34535  eulerpartlems  34537  eulerpartlemsv3  34538  eulerpartlemgc  34539  eulerpartlemv  34541  eulerpartlemgs2  34557  plymul02  34723  plymulx0  34724  itgexpif  34783  breprexplemc  34809  breprexp  34810  logdivsqrle  34827  subfacp1lem6  35398  cvxpconn  35455  cvxsconn  35456  fwddifnp1  36378  lcmineqlem10  42402  deg1pow  42505  pell1234qrne0  43204  jm2.19lem3  43342  jm2.25  43350  flcidc  43521  relexpmulg  44060  radcnvrat  44664  dvconstbi  44684  binomcxplemnn0  44699  sineq0ALT  45286  fperiodmullem  45659  fprod0  45950  dvsinax  46265  dvasinbx  46272  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  dvnxpaek  46294  dvnmul  46295  itgsinexplem1  46306  dirkertrigeqlem2  46451  fourierdlem42  46501  fourierdlem83  46541  sqwvfoura  46580  fouriersw  46583  elaa2lem  46585  etransclem15  46601  etransclem24  46610  etransclem35  46621  etransclem46  46632  sigarcol  47216  sharhght  47217  modlt0b  47717  fmtnofac2  47923  rrx2linest  49096  line2x  49108  line2y  49109  itschlc0yqe  49114  itschlc0xyqsol1  49120  itschlc0xyqsol  49121  2itscp  49135  aacllem  50154