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

Theorem mul02d 9831
Description: Multiplication by 0. Theorem I.6 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
mul02d  |-  ( ph  ->  ( 0  x.  A
)  =  0 )

Proof of Theorem mul02d
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 mul02 9811 . 2  |-  ( A  e.  CC  ->  (
0  x.  A )  =  0 )
31, 2syl 17 1  |-  ( ph  ->  ( 0  x.  A
)  =  0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444    e. wcel 1887  (class class class)co 6290   CCcc 9537   0cc0 9539    x. cmul 9544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-po 4755  df-so 4756  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9677  df-mnf 9678  df-ltxr 9680
This theorem is referenced by:  mulneg1  10055  mulge0  10132  mul0or  10252  prodgt0  10450  un0mulcl  10904  mul2lt0rgt0  11399  mul2lt0bi  11402  lincmb01cmp  11775  iccf1o  11776  discr1  12408  discr  12409  hashxplem  12605  cshweqrep  12920  remul2  13193  immul2  13200  binomlem  13887  geomulcvg  13932  ntrivcvgfvn0  13955  fprodeq0  14029  fprodeq0g  14048  0fallfac  14090  binomfallfaclem2  14093  efne0  14151  dvds0  14318  mulmoddvds  14363  smumullem  14466  mulgcd  14514  lcmgcd  14572  qnumgt0  14699  pcexp  14809  vdwapun  14924  vdwlem1  14931  mulgnn0ass  16787  odmulg  17207  torsubg  17492  isabvd  18048  nn0srg  19037  rge0srg  19038  prmirredlem  19064  nmo0  21756  nmoeq0  21757  blcvx  21816  reparphti  22028  pcorevlem  22057  ipcau2  22208  rrxcph  22351  itg1addlem4  22657  itg1addlem5  22658  itg1mulc  22662  itg2mulc  22705  dvcmul  22898  dvmptcmul  22918  dvexp3  22930  dvef  22932  dveq0  22952  dv11cn  22953  ply1termlem  23157  plyeq0lem  23164  plypf1  23166  plyaddlem1  23167  plymullem1  23168  coeeulem  23178  coeidlem  23191  coeid3  23194  coemullem  23204  coemulhi  23208  coemulc  23209  dgrco  23229  vieta1lem2  23264  elqaalem2  23273  elqaalem2OLD  23276  aalioulem3  23290  taylthlem2  23329  abelthlem6  23391  pilem2  23407  pilem2OLD  23408  sinhalfpip  23447  sinhalfpim  23448  coshalfpip  23449  coshalfpim  23450  logtayl  23605  mulcxp  23630  cxpmul2  23634  cxpeq  23697  chordthmlem5  23762  cubic  23775  atans2  23857  atantayl2  23864  leibpi  23868  efrlim  23895  scvxcvx  23911  amgm  23916  ftalem5  24001  ftalem5OLD  24003  basellem2  24008  mumul  24108  muinv  24122  dchrn0  24178  dchrinvcl  24181  lgsdirnn0  24267  lgsdinn0  24268  lgsquad2lem2  24287  rpvmasumlem  24325  dchrisum0flblem1  24346  rpvmasum2  24350  ostth2lem2  24472  brbtwn2  24935  axsegconlem1  24947  axpaschlem  24970  axcontlem7  25000  axcontlem8  25001  nvz0  26297  ipasslem1  26472  hi01  26749  xrge0iifhom  28743  indsum  28844  eulerpartlemsv2  29191  eulerpartlems  29193  eulerpartlemsv3  29194  eulerpartlemgc  29195  eulerpartlemv  29197  eulerpartlemgs2  29213  sgnmul  29413  plymul02  29435  plymulx0  29436  subfacp1lem6  29908  cvxpcon  29965  cvxscon  29966  fwddifnp1  30932  pell1234qrne0  35699  bezoutr1  35836  jm2.19lem3  35846  jm2.25  35854  flcidc  36040  relexpmulg  36302  radcnvrat  36663  dvconstbi  36683  binomcxplemnn0  36698  sineq0ALT  37334  fperiodmullem  37521  fprod0  37676  dvsinax  37783  dvasinbx  37792  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  dvnxpaek  37817  dvnmul  37818  itgsinexplem1  37830  dirkertrigeqlem2  37961  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem83  38053  sqwvfoura  38092  fouriersw  38095  elaa2lem  38097  elaa2lemOLD  38098  etransclem15  38114  etransclem24  38123  etransclem35  38134  etransclem46  38145  sigarcol  38473  sharhght  38474  aacllem  40593
  Copyright terms: Public domain W3C validator