Theorem mul02d 11372

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  0cc0 11068   · cmul 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213

This theorem is referenced by:  mulneg1  11614  mulge0  11696  mul0or  11818  prodgt0  12029  un0mulcl  12476  mul2lt0rgt0  13056  mul2lt0bi  13059  lincmb01cmp  13456  iccf1o  13457  discr1  14204  discr  14205  hashxplem  14398  cshweqrep  14786  remul2  15096  immul2  15103  binomlem  15795  geomulcvg  15842  ntrivcvgfvn0  15865  fprodeq0  15941  fprodeq0g  15960  0fallfac  16003  binomfallfaclem2  16006  efne0d  16063  efne0OLD  16065  dvds0  16241  pwp1fsum  16361  smumullem  16462  mulgcd  16518  bezoutr1  16539  lcmgcd  16577  qnumgt0  16720  pcexp  16830  vdwapun  16945  vdwlem1  16952  mulgnn0ass  19042  odmulg  19486  torsubg  19784  isabvd  20721  nn0srg  21354  rge0srg  21355  prmirredlem  21382  pzriprnglem8  21398  nmo0  24623  nmoeq0  24624  blcvx  24686  reparphti  24896  reparphtiOLD  24897  pcorevlem  24926  ipcau2  25134  rrxcph  25292  itg1addlem4  25600  itg1addlem5  25601  itg1mulc  25605  itg2mulc  25648  dvcmul  25847  dvmptcmul  25868  dvexp3  25882  dvef  25884  dveq0  25905  dv11cn  25906  ply1termlem  26108  plyeq0lem  26115  plypf1  26117  plyaddlem1  26118  plymullem1  26119  coeeulem  26129  coeidlem  26142  coeid3  26145  coemullem  26155  coemulhi  26159  coemulc  26160  dgrco  26181  vieta1lem2  26219  elqaalem2  26228  aalioulem3  26242  taylthlem2  26282  taylthlem2OLD  26283  abelthlem6  26346  pilem2  26362  sinhalfpip  26401  sinhalfpim  26402  coshalfpip  26403  coshalfpim  26404  logtayl  26569  mulcxp  26594  cxpmul2  26598  cxpeq  26667  chordthmlem5  26746  cubic  26759  atans2  26841  atantayl2  26848  leibpi  26852  efrlim  26879  efrlimOLD  26880  scvxcvx  26896  amgm  26901  ftalem5  26987  basellem2  26992  mumul  27091  muinv  27103  dchrn0  27161  dchrinvcl  27164  lgsdirnn0  27255  lgsdinn0  27256  lgsquad2lem2  27296  rpvmasumlem  27398  dchrisum0flblem1  27419  rpvmasum2  27423  ostth2lem2  27545  brbtwn2  28832  axsegconlem1  28844  axpaschlem  28867  axcontlem7  28897  axcontlem8  28898  elntg2  28912  nvz0  30597  ipasslem1  30760  hi01  31025  fprodeq02  32748  sgnmul  32760  indsum  32784  indsumin  32785  constrrtcc  33725  constrsslem  33731  constrremulcl  33757  2sqr3minply  33770  cos9thpiminplylem2  33773  xrge0iifhom  33927  eulerpartlemsv2  34349  eulerpartlems  34351  eulerpartlemsv3  34352  eulerpartlemgc  34353  eulerpartlemv  34355  eulerpartlemgs2  34371  plymul02  34537  plymulx0  34538  itgexpif  34597  breprexplemc  34623  breprexp  34624  logdivsqrle  34641  subfacp1lem6  35172  cvxpconn  35229  cvxsconn  35230  fwddifnp1  36153  lcmineqlem10  42026  deg1pow  42129  pell1234qrne0  42841  jm2.19lem3  42980  jm2.25  42988  flcidc  43159  relexpmulg  43699  radcnvrat  44303  dvconstbi  44323  binomcxplemnn0  44338  sineq0ALT  44926  fperiodmullem  45301  fprod0  45594  dvsinax  45911  dvasinbx  45918  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnxpaek  45940  dvnmul  45941  itgsinexplem1  45952  dirkertrigeqlem2  46097  fourierdlem42  46147  fourierdlem83  46187  sqwvfoura  46226  fouriersw  46229  elaa2lem  46231  etransclem15  46247  etransclem24  46256  etransclem35  46267  etransclem46  46278  sigarcol  46862  sharhght  46863  modlt0b  47364  fmtnofac2  47570  rrx2linest  48731  line2x  48743  line2y  48744  itschlc0yqe  48749  itschlc0xyqsol1  48755  itschlc0xyqsol  48756  2itscp  48770  aacllem  49790