Theorem mul02d 11459

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  0cc0 11155   · cmul 11160

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300

This theorem is referenced by:  mulneg1  11699  mulge0  11781  mul0or  11903  prodgt0  12114  un0mulcl  12560  mul2lt0rgt0  13138  mul2lt0bi  13141  lincmb01cmp  13535  iccf1o  13536  discr1  14278  discr  14279  hashxplem  14472  cshweqrep  14859  remul2  15169  immul2  15176  binomlem  15865  geomulcvg  15912  ntrivcvgfvn0  15935  fprodeq0  16011  fprodeq0g  16030  0fallfac  16073  binomfallfaclem2  16076  efne0  16133  dvds0  16309  pwp1fsum  16428  smumullem  16529  mulgcd  16585  bezoutr1  16606  lcmgcd  16644  qnumgt0  16787  pcexp  16897  vdwapun  17012  vdwlem1  17019  mulgnn0ass  19128  odmulg  19574  torsubg  19872  isabvd  20813  nn0srg  21455  rge0srg  21456  prmirredlem  21483  pzriprnglem8  21499  nmo0  24756  nmoeq0  24757  blcvx  24819  reparphti  25029  reparphtiOLD  25030  pcorevlem  25059  ipcau2  25268  rrxcph  25426  itg1addlem4  25734  itg1addlem5  25735  itg1mulc  25739  itg2mulc  25782  dvcmul  25981  dvmptcmul  26002  dvexp3  26016  dvef  26018  dveq0  26039  dv11cn  26040  ply1termlem  26242  plyeq0lem  26249  plypf1  26251  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  coeidlem  26276  coeid3  26279  coemullem  26289  coemulhi  26293  coemulc  26294  dgrco  26315  vieta1lem2  26353  elqaalem2  26362  aalioulem3  26376  taylthlem2  26416  taylthlem2OLD  26417  abelthlem6  26480  pilem2  26496  sinhalfpip  26534  sinhalfpim  26535  coshalfpip  26536  coshalfpim  26537  logtayl  26702  mulcxp  26727  cxpmul2  26731  cxpeq  26800  chordthmlem5  26879  cubic  26892  atans2  26974  atantayl2  26981  leibpi  26985  efrlim  27012  efrlimOLD  27013  scvxcvx  27029  amgm  27034  ftalem5  27120  basellem2  27125  mumul  27224  muinv  27236  dchrn0  27294  dchrinvcl  27297  lgsdirnn0  27388  lgsdinn0  27389  lgsquad2lem2  27429  rpvmasumlem  27531  dchrisum0flblem1  27552  rpvmasum2  27556  ostth2lem2  27678  brbtwn2  28920  axsegconlem1  28932  axpaschlem  28955  axcontlem7  28985  axcontlem8  28986  elntg2  29000  nvz0  30687  ipasslem1  30850  hi01  31115  fprodeq02  32825  indsum  32846  indsumin  32847  constrrtcc  33776  constrsslem  33782  2sqr3minply  33791  xrge0iifhom  33936  eulerpartlemsv2  34360  eulerpartlems  34362  eulerpartlemsv3  34363  eulerpartlemgc  34364  eulerpartlemv  34366  eulerpartlemgs2  34382  sgnmul  34545  plymul02  34561  plymulx0  34562  itgexpif  34621  breprexplemc  34647  breprexp  34648  logdivsqrle  34665  subfacp1lem6  35190  cvxpconn  35247  cvxsconn  35248  fwddifnp1  36166  lcmineqlem10  42039  deg1pow  42142  efne0d  42373  pell1234qrne0  42864  jm2.19lem3  43003  jm2.25  43011  flcidc  43182  relexpmulg  43723  radcnvrat  44333  dvconstbi  44353  binomcxplemnn0  44368  sineq0ALT  44957  fperiodmullem  45315  fprod0  45611  dvsinax  45928  dvasinbx  45935  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnxpaek  45957  dvnmul  45958  itgsinexplem1  45969  dirkertrigeqlem2  46114  fourierdlem42  46164  fourierdlem83  46204  sqwvfoura  46243  fouriersw  46246  elaa2lem  46248  etransclem15  46264  etransclem24  46273  etransclem35  46284  etransclem46  46295  sigarcol  46879  sharhght  46880  fmtnofac2  47556  rrx2linest  48663  line2x  48675  line2y  48676  itschlc0yqe  48681  itschlc0xyqsol1  48687  itschlc0xyqsol  48688  2itscp  48702  aacllem  49320