Theorem mul02d 11396

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086  0cc0 11088   · cmul 11093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-ltxr 11236

This theorem is referenced by:  mulneg1  11638  mulge0  11720  mul0or  11842  prodgt0  12050  un0mulcl  12526  mul2lt0rgt0  13109  mul2lt0bi  13112  lincmb01cmp  13510  iccf1o  13511  discr1  14263  discr  14264  hashxplem  14458  cshweqrep  14846  sgnmul  15132  remul2  15169  immul2  15176  indsum  15868  binomlem  15871  geomulcvg  15918  ntrivcvgfvn0  15941  fprodeq0  16017  fprodeq0g  16036  0fallfac  16079  binomfallfaclem2  16082  efne0d  16139  efne0OLD  16141  dvds0  16317  pwp1fsum  16437  smumullem  16538  mulgcd  16594  bezoutr1  16615  lcmgcd  16653  qnumgt0  16797  pcexp  16907  vdwapun  17022  vdwlem1  17029  mulgnn0ass  19164  odmulg  19614  torsubg  19912  isabvd  20881  nn0srg  21544  rge0srg  21545  prmirredlem  21579  pzriprnglem8  21595  nmo0  24849  nmoeq0  24850  blcvx  24912  reparphti  25113  pcorevlem  25142  ipcau2  25350  rrxcph  25508  itg1addlem4  25815  itg1addlem5  25816  itg1mulc  25820  itg2mulc  25863  dvcmul  26060  dvmptcmul  26080  dvexp3  26094  dvef  26096  dveq0  26116  dv11cn  26117  ply1termlem  26317  plyeq0lem  26324  plypf1  26326  plyaddlem1  26327  plymullem1  26328  coeeulem  26338  coeidlem  26351  coeid3  26354  coemullem  26364  coemulhi  26368  coemulc  26369  dgrco  26389  plymul02  26398  plyn0mulidp  26399  vieta1lem2  26429  elqaalem2  26438  aalioulem3  26452  taylthlem2  26491  abelthlem6  26553  pilem2  26569  sinhalfpip  26611  sinhalfpim  26612  coshalfpip  26613  coshalfpim  26614  logtayl  26779  mulcxp  26804  cxpmul2  26808  cxpeq  26876  chordthmlem5  26955  cubic  26968  atans2  27050  atantayl2  27057  leibpi  27061  efrlim  27088  scvxcvx  27104  amgm  27109  ftalem5  27195  basellem2  27200  mumul  27299  muinv  27311  dchrn0  27368  dchrinvcl  27371  lgsdirnn0  27462  lgsdinn0  27463  lgsquad2lem2  27503  rpvmasumlem  27605  dchrisum0flblem1  27626  rpvmasum2  27630  ostth2lem2  27752  brbtwn2  29160  axsegconlem1  29172  axpaschlem  29195  axcontlem7  29225  axcontlem8  29226  elntg2  29240  nvz0  30925  ipasslem1  31088  hi01  31353  fprodeq02  33076  indsumin  33089  constrrtcc  34037  constrsslem  34043  constrremulcl  34069  2sqr3minply  34082  cos9thpiminplylem2  34085  xrge0iifhom  34239  eulerpartlemsv2  34660  eulerpartlems  34662  eulerpartlemsv3  34663  eulerpartlemgc  34664  eulerpartlemv  34666  eulerpartlemgs2  34682  itgexpif  34905  breprexplemc  34931  breprexp  34932  logdivsqrle  34949  subfacp1lem6  35543  cvxpconn  35600  cvxsconn  35601  fwddifnp1  36523  lcmineqlem10  42662  deg1pow  42765  pell1234qrne0  43437  jm2.19lem3  43575  jm2.25  43583  flcidc  43754  relexpmulg  44293  radcnvrat  44883  dvconstbi  44903  binomcxplemnn0  44918  sineq0ALT  45504  fperiodmullem  45881  fprod0  46171  dvsinax  46486  dvasinbx  46493  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  dvnxpaek  46515  dvnmul  46516  itgsinexplem1  46527  dirkertrigeqlem2  46672  fourierdlem42  46722  fourierdlem83  46762  sqwvfoura  46801  fouriersw  46804  elaa2lem  46806  etransclem15  46822  etransclem24  46831  etransclem35  46842  etransclem46  46853  sigarcol  47437  sharhght  47438  modlt0b  47962  fmtnofac2  48177  rrx2linest  49374  line2x  49386  line2y  49387  itschlc0yqe  49392  itschlc0xyqsol1  49398  itschlc0xyqsol  49399  2itscp  49413  aacllem  50431