Theorem mul02d 10881

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7155  ℂcc 10578  0cc0 10580   · cmul 10585

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-resscn 10637  ax-1cn 10638  ax-icn 10639  ax-addcl 10640  ax-addrcl 10641  ax-mulcl 10642  ax-mulrcl 10643  ax-mulcom 10644  ax-addass 10645  ax-mulass 10646  ax-distr 10647  ax-i2m1 10648  ax-1ne0 10649  ax-1rid 10650  ax-rnegex 10651  ax-rrecex 10652  ax-cnre 10653  ax-pre-lttri 10654  ax-pre-lttrn 10655  ax-pre-ltadd 10656

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-po 5446  df-so 5447  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-ov 7158  df-er 8304  df-en 8533  df-dom 8534  df-sdom 8535  df-pnf 10720  df-mnf 10721  df-ltxr 10723

This theorem is referenced by:  mulneg1  11119  mulge0  11201  mul0or  11323  prodgt0  11530  un0mulcl  11973  mul2lt0rgt0  12538  mul2lt0bi  12541  lincmb01cmp  12932  iccf1o  12933  discr1  13655  discr  13656  hashxplem  13849  cshweqrep  14235  remul2  14542  immul2  14549  binomlem  15237  pwm1geoserOLD  15278  geomulcvg  15285  ntrivcvgfvn0  15308  fprodeq0  15382  fprodeq0g  15401  0fallfac  15444  binomfallfaclem2  15447  efne0  15503  dvds0  15678  pwp1fsum  15797  smumullem  15896  mulgcd  15952  bezoutr1  15970  lcmgcd  16008  qnumgt0  16150  pcexp  16256  vdwapun  16370  vdwlem1  16377  mulgnn0ass  18335  odmulg  18755  torsubg  19047  isabvd  19664  nn0srg  20241  rge0srg  20242  prmirredlem  20267  nmo0  23442  nmoeq0  23443  blcvx  23504  reparphti  23703  pcorevlem  23732  ipcau2  23939  rrxcph  24097  itg1addlem4  24404  itg1addlem5  24405  itg1mulc  24409  itg2mulc  24452  dvcmul  24648  dvmptcmul  24668  dvexp3  24682  dvef  24684  dveq0  24704  dv11cn  24705  ply1termlem  24904  plyeq0lem  24911  plypf1  24913  plyaddlem1  24914  plymullem1  24915  coeeulem  24925  coeidlem  24938  coeid3  24941  coemullem  24951  coemulhi  24955  coemulc  24956  dgrco  24976  vieta1lem2  25011  elqaalem2  25020  aalioulem3  25034  taylthlem2  25073  abelthlem6  25135  pilem2  25151  sinhalfpip  25189  sinhalfpim  25190  coshalfpip  25191  coshalfpim  25192  logtayl  25355  mulcxp  25380  cxpmul2  25384  cxpeq  25450  chordthmlem5  25526  cubic  25539  atans2  25621  atantayl2  25628  leibpi  25632  efrlim  25659  scvxcvx  25675  amgm  25680  ftalem5  25766  basellem2  25771  mumul  25870  muinv  25882  dchrn0  25938  dchrinvcl  25941  lgsdirnn0  26032  lgsdinn0  26033  lgsquad2lem2  26073  rpvmasumlem  26175  dchrisum0flblem1  26196  rpvmasum2  26200  ostth2lem2  26322  brbtwn2  26803  axsegconlem1  26815  axpaschlem  26838  axcontlem7  26868  axcontlem8  26869  elntg2  26883  nvz0  28555  ipasslem1  28718  hi01  28983  fprodeq02  30665  xrge0iifhom  31412  indsum  31512  indsumin  31513  eulerpartlemsv2  31848  eulerpartlems  31850  eulerpartlemsv3  31851  eulerpartlemgc  31852  eulerpartlemv  31854  eulerpartlemgs2  31870  sgnmul  32032  plymul02  32048  plymulx0  32049  itgexpif  32109  breprexplemc  32135  breprexp  32136  logdivsqrle  32153  subfacp1lem6  32667  cvxpconn  32724  cvxsconn  32725  fwddifnp1  34042  lcmineqlem10  39631  pell1234qrne0  40195  jm2.19lem3  40333  jm2.25  40341  flcidc  40519  relexpmulg  40812  radcnvrat  41419  dvconstbi  41439  binomcxplemnn0  41454  sineq0ALT  42044  fperiodmullem  42331  fprod0  42632  dvsinax  42949  dvasinbx  42956  ioodvbdlimc1lem2  42968  ioodvbdlimc2lem  42970  dvnxpaek  42978  dvnmul  42979  itgsinexplem1  42990  dirkertrigeqlem2  43135  fourierdlem42  43185  fourierdlem83  43225  sqwvfoura  43264  fouriersw  43267  elaa2lem  43269  etransclem15  43285  etransclem24  43294  etransclem35  43305  etransclem46  43316  sigarcol  43872  sharhght  43873  fmtnofac2  44482  rrx2linest  45549  line2x  45561  line2y  45562  itschlc0yqe  45567  itschlc0xyqsol1  45573  itschlc0xyqsol  45574  2itscp  45588  aacllem  45793