Theorem mul02d 11512

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7421  ℂcc 11202  0cc0 11204   · cmul 11209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-resscn 11261  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-addrcl 11265  ax-mulcl 11266  ax-mulrcl 11267  ax-mulcom 11268  ax-addass 11269  ax-mulass 11270  ax-distr 11271  ax-i2m1 11272  ax-1ne0 11273  ax-1rid 11274  ax-rnegex 11275  ax-rrecex 11276  ax-cnre 11277  ax-pre-lttri 11278  ax-pre-lttrn 11279  ax-pre-ltadd 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-ltxr 11352

This theorem is used by:  mulneg1  11756  mulge0  11838  mul0or  11960  prodgt0  12168  un0mulcl  12644  mul2lt0rgt0  13229  mul2lt0bi  13232  lincmb01cmp  13630  iccf1o  13631  discr1  14387  discr  14388  hashxplem  14582  cshweqrep  14977  sgnmul  15266  remul2  15303  immul2  15310  indsum  16001  binomlem  16004  geomulcvg  16051  ntrivcvgfvn0  16074  fprodeq0  16148  fprodeq0g  16167  0fallfac  16209  binomfallfaclem2  16212  efne0d  16269  efne0OLD  16271  dvds0  16447  pwp1fsum  16567  smumullem  16668  mulgcd  16727  bezoutr1  16750  lcmgcd  16788  qnumgt0  16932  pcexp  17043  vdwapun  17158  vdwlem1  17165  mulgnn0ass  19326  odmulg  19776  torsubg  20074  isabvd  21075  nn0srg  21749  rge0srg  21750  prmirredlem  21784  pzriprnglem8  21800  nmo0  25060  nmoeq0  25061  blcvx  25123  reparphti  25324  pcorevlem  25353  ipcau2  25561  rrxcph  25719  itg1addlem4  26026  itg1addlem5  26027  itg1mulc  26031  itg2mulc  26074  dvcmul  26270  dvmptcmul  26290  dvexp3  26304  dvef  26306  dveq0  26326  dv11cn  26327  ply1termlem  26527  plyeq0lem  26535  plypf1  26537  plyaddlem1  26538  plymullem1  26539  coeeulem  26549  coeidlem  26562  coeid3  26565  coemullem  26575  coemulhi  26579  coemulc  26580  dgrco  26600  plymul02  26607  plyn0mulidp  26608  vieta1lem2  26640  elqaalem2  26649  aalioulem3  26667  taylthlem2  26707  abelthlem6  26769  pilem2  26785  sinhalfpip  26827  sinhalfpim  26828  coshalfpip  26829  coshalfpim  26830  logtayl  26994  mulcxp  27019  cxpmul2  27023  cxpeq  27091  chordthmlem5  27170  cubic  27183  atans2  27265  atantayl2  27272  leibpi  27276  efrlim  27303  scvxcvx  27319  amgm  27324  ftalem5  27410  basellem2  27415  mumul  27514  muinv  27526  dchrn0  27583  dchrinvcl  27586  lgsdirnn0  27677  lgsdinn0  27678  lgsquad2lem2  27718  rpvmasumlem  27820  dchrisum0flblem1  27841  rpvmasum2  27845  ostth2lem2  27967  brbtwn2  29489  axsegconlem1  29501  axpaschlem  29524  axcontlem7  29554  axcontlem8  29555  elntg2  29569  nvz0  31276  ipasslem1  31439  hi01  31704  fprodeq02  33462  indsumin  33475  constrrtcc  34414  constrsslem  34420  constrremulcl  34446  2sqr3minply  34459  cos9thpiminplylem2  34462  xrge0iifhom  34616  eulerpartlemsv2  35037  eulerpartlems  35039  eulerpartlemsv3  35040  eulerpartlemgc  35041  eulerpartlemv  35043  eulerpartlemgs2  35059  itgexpif  35282  breprexplemc  35308  breprexp  35309  logdivsqrle  35326  subfacp1lem6  36037  cvxpconn  36094  cvxsconn  36095  fwddifnp1  37023  lcmineqlem10  43182  deg1pow  43285  pell1234qrne0  43954  jm2.19lem3  44092  jm2.25  44100  flcidc  44266  relexpmulg  44804  radcnvrat  45392  dvconstbi  45412  binomcxplemnn0  45427  sineq0ALT  46013  fperiodmullem  46413  fprod0  46702  dvsinax  47017  dvasinbx  47024  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnxpaek  47046  dvnmul  47047  itgsinexplem1  47058  dirkertrigeqlem2  47203  fourierdlem42  47253  fourierdlem83  47293  sqwvfoura  47332  fouriersw  47335  elaa2lem  47337  etransclem15  47353  etransclem24  47362  etransclem35  47373  etransclem46  47384  sigarcol  47968  sharhght  47969  modlt0b  48533  fmtnofac2  48748  rrx2linest  49948  line2x  49960  line2y  49961  itschlc0yqe  49966  itschlc0xyqsol1  49972  itschlc0xyqsol  49973  2itscp  49987  aacllem  51108