Theorem mul02d 11344

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂ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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  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 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 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184

This theorem is referenced by:  mulneg1  11586  mulge0  11668  mul0or  11790  prodgt0  12002  un0mulcl  12471  mul2lt0rgt0  13047  mul2lt0bi  13050  lincmb01cmp  13448  iccf1o  13449  discr1  14201  discr  14202  hashxplem  14395  cshweqrep  14783  remul2  15092  immul2  15099  indsum  15791  binomlem  15794  geomulcvg  15841  ntrivcvgfvn0  15864  fprodeq0  15940  fprodeq0g  15959  0fallfac  16002  binomfallfaclem2  16005  efne0d  16062  efne0OLD  16064  dvds0  16240  pwp1fsum  16360  smumullem  16461  mulgcd  16517  bezoutr1  16538  lcmgcd  16576  qnumgt0  16720  pcexp  16830  vdwapun  16945  vdwlem1  16952  mulgnn0ass  19086  odmulg  19531  torsubg  19829  isabvd  20789  nn0srg  21417  rge0srg  21418  prmirredlem  21452  pzriprnglem8  21468  nmo0  24700  nmoeq0  24701  blcvx  24763  reparphti  24964  pcorevlem  24993  ipcau2  25201  rrxcph  25359  itg1addlem4  25666  itg1addlem5  25667  itg1mulc  25671  itg2mulc  25714  dvcmul  25911  dvmptcmul  25931  dvexp3  25945  dvef  25947  dveq0  25967  dv11cn  25968  ply1termlem  26168  plyeq0lem  26175  plypf1  26177  plyaddlem1  26178  plymullem1  26179  coeeulem  26189  coeidlem  26202  coeid3  26205  coemullem  26215  coemulhi  26219  coemulc  26220  dgrco  26240  vieta1lem2  26277  elqaalem2  26286  aalioulem3  26300  taylthlem2  26339  abelthlem6  26401  pilem2  26417  sinhalfpip  26456  sinhalfpim  26457  coshalfpip  26458  coshalfpim  26459  logtayl  26624  mulcxp  26649  cxpmul2  26653  cxpeq  26721  chordthmlem5  26800  cubic  26813  atans2  26895  atantayl2  26902  leibpi  26906  efrlim  26933  scvxcvx  26949  amgm  26954  ftalem5  27040  basellem2  27045  mumul  27144  muinv  27156  dchrn0  27213  dchrinvcl  27216  lgsdirnn0  27307  lgsdinn0  27308  lgsquad2lem2  27348  rpvmasumlem  27450  dchrisum0flblem1  27471  rpvmasum2  27475  ostth2lem2  27597  brbtwn2  28974  axsegconlem1  28986  axpaschlem  29009  axcontlem7  29039  axcontlem8  29040  elntg2  29054  nvz0  30739  ipasslem1  30902  hi01  31167  fprodeq02  32897  sgnmul  32908  indsumin  32921  constrrtcc  33879  constrsslem  33885  constrremulcl  33911  2sqr3minply  33924  cos9thpiminplylem2  33927  xrge0iifhom  34081  eulerpartlemsv2  34502  eulerpartlems  34504  eulerpartlemsv3  34505  eulerpartlemgc  34506  eulerpartlemv  34508  eulerpartlemgs2  34524  plymul02  34690  plymulx0  34691  itgexpif  34750  breprexplemc  34776  breprexp  34777  logdivsqrle  34794  subfacp1lem6  35367  cvxpconn  35424  cvxsconn  35425  fwddifnp1  36347  lcmineqlem10  42477  deg1pow  42580  pell1234qrne0  43281  jm2.19lem3  43419  jm2.25  43427  flcidc  43598  relexpmulg  44137  radcnvrat  44741  dvconstbi  44761  binomcxplemnn0  44776  sineq0ALT  45363  fperiodmullem  45736  fprod0  46026  dvsinax  46341  dvasinbx  46348  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnxpaek  46370  dvnmul  46371  itgsinexplem1  46382  dirkertrigeqlem2  46527  fourierdlem42  46577  fourierdlem83  46617  sqwvfoura  46656  fouriersw  46659  elaa2lem  46661  etransclem15  46677  etransclem24  46686  etransclem35  46697  etransclem46  46708  sigarcol  47292  sharhght  47293  modlt0b  47817  fmtnofac2  48032  rrx2linest  49218  line2x  49230  line2y  49231  itschlc0yqe  49236  itschlc0xyqsol1  49242  itschlc0xyqsol  49243  2itscp  49257  aacllem  50276