Theorem mul02d 11444

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7419  ℂcc 11138  0cc0 11140   · cmul 11145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-ltxr 11285

This theorem is referenced by:  mulneg1  11682  mulge0  11764  mul0or  11886  prodgt0  12094  un0mulcl  12539  mul2lt0rgt0  13112  mul2lt0bi  13115  lincmb01cmp  13507  iccf1o  13508  discr1  14237  discr  14238  hashxplem  14428  cshweqrep  14807  remul2  15113  immul2  15120  binomlem  15811  geomulcvg  15858  ntrivcvgfvn0  15881  fprodeq0  15955  fprodeq0g  15974  0fallfac  16017  binomfallfaclem2  16020  efne0  16077  dvds0  16252  pwp1fsum  16371  smumullem  16470  mulgcd  16527  bezoutr1  16543  lcmgcd  16581  qnumgt0  16725  pcexp  16831  vdwapun  16946  vdwlem1  16953  mulgnn0ass  19073  odmulg  19523  torsubg  19821  isabvd  20712  nn0srg  21387  rge0srg  21388  prmirredlem  21415  pzriprnglem8  21431  nmo0  24696  nmoeq0  24697  blcvx  24758  reparphti  24967  reparphtiOLD  24968  pcorevlem  24997  ipcau2  25206  rrxcph  25364  itg1addlem4  25672  itg1addlem4OLD  25673  itg1addlem5  25674  itg1mulc  25678  itg2mulc  25721  dvcmul  25919  dvmptcmul  25940  dvexp3  25954  dvef  25956  dveq0  25977  dv11cn  25978  ply1termlem  26182  plyeq0lem  26189  plypf1  26191  plyaddlem1  26192  plymullem1  26193  coeeulem  26203  coeidlem  26216  coeid3  26219  coemullem  26229  coemulhi  26233  coemulc  26234  dgrco  26255  vieta1lem2  26291  elqaalem2  26300  aalioulem3  26314  taylthlem2  26354  taylthlem2OLD  26355  abelthlem6  26418  pilem2  26434  sinhalfpip  26472  sinhalfpim  26473  coshalfpip  26474  coshalfpim  26475  logtayl  26639  mulcxp  26664  cxpmul2  26668  cxpeq  26737  chordthmlem5  26813  cubic  26826  atans2  26908  atantayl2  26915  leibpi  26919  efrlim  26946  efrlimOLD  26947  scvxcvx  26963  amgm  26968  ftalem5  27054  basellem2  27059  mumul  27158  muinv  27170  dchrn0  27228  dchrinvcl  27231  lgsdirnn0  27322  lgsdinn0  27323  lgsquad2lem2  27363  rpvmasumlem  27465  dchrisum0flblem1  27486  rpvmasum2  27490  ostth2lem2  27612  brbtwn2  28788  axsegconlem1  28800  axpaschlem  28823  axcontlem7  28853  axcontlem8  28854  elntg2  28868  nvz0  30550  ipasslem1  30713  hi01  30978  fprodeq02  32671  xrge0iifhom  33669  indsum  33771  indsumin  33772  eulerpartlemsv2  34109  eulerpartlems  34111  eulerpartlemsv3  34112  eulerpartlemgc  34113  eulerpartlemv  34115  eulerpartlemgs2  34131  sgnmul  34293  plymul02  34309  plymulx0  34310  itgexpif  34369  breprexplemc  34395  breprexp  34396  logdivsqrle  34413  subfacp1lem6  34926  cvxpconn  34983  cvxsconn  34984  fwddifnp1  35892  lcmineqlem10  41641  deg1pow  41744  efne0d  42043  pell1234qrne0  42415  jm2.19lem3  42554  jm2.25  42562  flcidc  42740  relexpmulg  43282  radcnvrat  43893  dvconstbi  43913  binomcxplemnn0  43928  sineq0ALT  44518  fperiodmullem  44823  fprod0  45122  dvsinax  45439  dvasinbx  45446  ioodvbdlimc1lem2  45458  ioodvbdlimc2lem  45460  dvnxpaek  45468  dvnmul  45469  itgsinexplem1  45480  dirkertrigeqlem2  45625  fourierdlem42  45675  fourierdlem83  45715  sqwvfoura  45754  fouriersw  45757  elaa2lem  45759  etransclem15  45775  etransclem24  45784  etransclem35  45795  etransclem46  45806  sigarcol  46390  sharhght  46391  fmtnofac2  47046  rrx2linest  48001  line2x  48013  line2y  48014  itschlc0yqe  48019  itschlc0xyqsol1  48025  itschlc0xyqsol  48026  2itscp  48040  aacllem  48420