Theorem mul02d 11409

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099  0cc0 11101   · cmul 11106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-ltxr 11249

This theorem is referenced by:  mulneg1  11651  mulge0  11733  mul0or  11855  prodgt0  12063  un0mulcl  12539  mul2lt0rgt0  13122  mul2lt0bi  13125  lincmb01cmp  13523  iccf1o  13524  discr1  14277  discr  14278  hashxplem  14472  cshweqrep  14860  sgnmul  15146  remul2  15183  immul2  15190  indsum  15882  binomlem  15885  geomulcvg  15932  ntrivcvgfvn0  15955  fprodeq0  16031  fprodeq0g  16050  0fallfac  16092  binomfallfaclem2  16095  efne0d  16152  efne0OLD  16154  dvds0  16330  pwp1fsum  16450  smumullem  16551  mulgcd  16607  bezoutr1  16628  lcmgcd  16666  qnumgt0  16810  pcexp  16920  vdwapun  17035  vdwlem1  17042  mulgnn0ass  19177  odmulg  19627  torsubg  19925  isabvd  20896  nn0srg  21568  rge0srg  21569  prmirredlem  21603  pzriprnglem8  21619  nmo0  24873  nmoeq0  24874  blcvx  24936  reparphti  25137  pcorevlem  25166  ipcau2  25374  rrxcph  25532  itg1addlem4  25839  itg1addlem5  25840  itg1mulc  25844  itg2mulc  25887  dvcmul  26084  dvmptcmul  26104  dvexp3  26118  dvef  26120  dveq0  26140  dv11cn  26141  ply1termlem  26341  plyeq0lem  26348  plypf1  26350  plyaddlem1  26351  plymullem1  26352  coeeulem  26362  coeidlem  26375  coeid3  26378  coemullem  26388  coemulhi  26392  coemulc  26393  dgrco  26413  plymul02  26422  plyn0mulidp  26423  vieta1lem2  26453  elqaalem2  26462  aalioulem3  26478  taylthlem2  26518  abelthlem6  26580  pilem2  26596  sinhalfpip  26638  sinhalfpim  26639  coshalfpip  26640  coshalfpim  26641  logtayl  26806  mulcxp  26831  cxpmul2  26835  cxpeq  26903  chordthmlem5  26982  cubic  26995  atans2  27077  atantayl2  27084  leibpi  27088  efrlim  27115  scvxcvx  27131  amgm  27136  ftalem5  27222  basellem2  27227  mumul  27326  muinv  27338  dchrn0  27395  dchrinvcl  27398  lgsdirnn0  27489  lgsdinn0  27490  lgsquad2lem2  27530  rpvmasumlem  27632  dchrisum0flblem1  27653  rpvmasum2  27657  ostth2lem2  27779  brbtwn2  29236  axsegconlem1  29248  axpaschlem  29271  axcontlem7  29301  axcontlem8  29302  elntg2  29316  nvz0  31001  ipasslem1  31164  hi01  31429  fprodeq02  33149  indsumin  33162  constrrtcc  34106  constrsslem  34112  constrremulcl  34138  2sqr3minply  34151  cos9thpiminplylem2  34154  xrge0iifhom  34308  eulerpartlemsv2  34729  eulerpartlems  34731  eulerpartlemsv3  34732  eulerpartlemgc  34733  eulerpartlemv  34735  eulerpartlemgs2  34751  itgexpif  34974  breprexplemc  35000  breprexp  35001  logdivsqrle  35018  subfacp1lem6  35658  cvxpconn  35715  cvxsconn  35716  fwddifnp1  36638  lcmineqlem10  42786  deg1pow  42889  pell1234qrne0  43563  jm2.19lem3  43701  jm2.25  43709  flcidc  43880  relexpmulg  44419  radcnvrat  45007  dvconstbi  45027  binomcxplemnn0  45042  sineq0ALT  45628  fperiodmullem  46005  fprod0  46295  dvsinax  46610  dvasinbx  46617  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  dvnxpaek  46639  dvnmul  46640  itgsinexplem1  46651  dirkertrigeqlem2  46796  fourierdlem42  46846  fourierdlem83  46886  sqwvfoura  46925  fouriersw  46928  elaa2lem  46930  etransclem15  46946  etransclem24  46955  etransclem35  46966  etransclem46  46977  sigarcol  47561  sharhght  47562  modlt0b  48089  fmtnofac2  48304  rrx2linest  49505  line2x  49517  line2y  49518  itschlc0yqe  49523  itschlc0xyqsol1  49529  itschlc0xyqsol  49530  2itscp  49544  aacllem  50584