MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mul02d Structured version   Visualization version   GIF version

Theorem mul02d 10219
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
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 mul02 10199 . 2 (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
31, 2syl 17 1 (𝜑 → (0 · 𝐴) = 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wcel 1988  (class class class)co 6635  cc 9919  0cc0 9921   · cmul 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-po 5025  df-so 5026  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-pnf 10061  df-mnf 10062  df-ltxr 10064
This theorem is referenced by:  mulneg1  10451  mulge0  10531  mul0or  10652  prodgt0  10853  un0mulcl  11312  mul2lt0rgt0  11918  mul2lt0bi  11921  lincmb01cmp  12300  iccf1o  12301  discr1  12983  discr  12984  hashxplem  13203  cshweqrep  13548  remul2  13851  immul2  13858  binomlem  14542  pwm1geoser  14581  geomulcvg  14588  ntrivcvgfvn0  14612  fprodeq0  14686  fprodeq0g  14706  0fallfac  14749  binomfallfaclem2  14752  efne0  14808  dvds0  14978  mulmoddvds  15032  pwp1fsum  15095  smumullem  15195  mulgcd  15246  bezoutr1  15263  lcmgcd  15301  qnumgt0  15439  pcexp  15545  vdwapun  15659  vdwlem1  15666  mulgnn0ass  17559  odmulg  17954  torsubg  18238  isabvd  18801  nn0srg  19797  rge0srg  19798  prmirredlem  19822  nmo0  22520  nmoeq0  22521  blcvx  22582  reparphti  22778  pcorevlem  22807  ipcau2  23014  rrxcph  23161  itg1addlem4  23447  itg1addlem5  23448  itg1mulc  23452  itg2mulc  23495  dvcmul  23688  dvmptcmul  23708  dvexp3  23722  dvef  23724  dveq0  23744  dv11cn  23745  ply1termlem  23940  plyeq0lem  23947  plypf1  23949  plyaddlem1  23950  plymullem1  23951  coeeulem  23961  coeidlem  23974  coeid3  23977  coemullem  23987  coemulhi  23991  coemulc  23992  dgrco  24012  vieta1lem2  24047  elqaalem2  24056  aalioulem3  24070  taylthlem2  24109  abelthlem6  24171  pilem2  24187  sinhalfpip  24225  sinhalfpim  24226  coshalfpip  24227  coshalfpim  24228  logtayl  24387  mulcxp  24412  cxpmul2  24416  cxpeq  24479  chordthmlem5  24544  cubic  24557  atans2  24639  atantayl2  24646  leibpi  24650  efrlim  24677  scvxcvx  24693  amgm  24698  ftalem5  24784  basellem2  24789  mumul  24888  muinv  24900  dchrn0  24956  dchrinvcl  24959  lgsdirnn0  25050  lgsdinn0  25051  lgsquad2lem2  25091  rpvmasumlem  25157  dchrisum0flblem1  25178  rpvmasum2  25182  ostth2lem2  25304  brbtwn2  25766  axsegconlem1  25778  axpaschlem  25801  axcontlem7  25831  axcontlem8  25832  nvz0  27493  ipasslem1  27656  hi01  27923  fprodeq02  29543  xrge0iifhom  29957  indsum  30057  indsumin  30058  eulerpartlemsv2  30394  eulerpartlems  30396  eulerpartlemsv3  30397  eulerpartlemgc  30398  eulerpartlemv  30400  eulerpartlemgs2  30416  sgnmul  30578  plymul02  30597  plymulx0  30598  itgexpif  30658  breprexplemc  30684  breprexp  30685  logdivsqrle  30702  subfacp1lem6  31141  cvxpconn  31198  cvxsconn  31199  fwddifnp1  32247  pell1234qrne0  37236  jm2.19lem3  37377  jm2.25  37385  flcidc  37563  relexpmulg  37821  radcnvrat  38333  dvconstbi  38353  binomcxplemnn0  38368  sineq0ALT  38993  fperiodmullem  39330  fprod0  39628  dvsinax  39890  dvasinbx  39898  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  dvnxpaek  39920  dvnmul  39921  itgsinexplem1  39932  dirkertrigeqlem2  40079  fourierdlem42  40129  fourierdlem83  40169  sqwvfoura  40208  fouriersw  40211  elaa2lem  40213  etransclem15  40229  etransclem24  40238  etransclem35  40249  etransclem46  40260  sigarcol  40816  sharhght  40817  fmtnofac2  41246  aacllem  42312
  Copyright terms: Public domain W3C validator