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

Theorem mulcli 9630
Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1  |-  A  e.  CC
axi.2  |-  B  e.  CC
Assertion
Ref Expression
mulcli  |-  ( A  x.  B )  e.  CC

Proof of Theorem mulcli
StepHypRef Expression
1 axi.1 . 2  |-  A  e.  CC
2 axi.2 . 2  |-  B  e.  CC
3 mulcl 9605 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3mp2an 670 1  |-  ( A  x.  B )  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1842  (class class class)co 6277   CCcc 9519    x. cmul 9526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9583
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  mul02lem2  9790  addid1  9793  cnegex2  9795  ixi  10218  2mulicn  10802  numma  11049  nummac  11050  decbin2  11122  irec  12310  binom2i  12320  crreczi  12333  nn0opthi  12392  faclbnd4lem1  12413  rei  13136  imi  13137  iseraltlem2  13652  bpoly3  14001  bpoly4  14002  odd2np1  14253  gcdaddmlem  14373  modxai  14761  mod2xnegi  14764  decexp2  14768  decsplit  14776  karatsuba  14777  sinhalfpilem  23146  ef2pi  23160  ef2kpi  23161  efper  23162  sinperlem  23163  sin2kpi  23166  cos2kpi  23167  sin2pim  23168  cos2pim  23169  sincos4thpi  23196  sincos6thpi  23198  pige3  23200  abssinper  23201  efeq1  23206  logneg  23265  logm1  23266  eflogeq  23279  logimul  23291  logneg2  23292  cxpsqrt  23376  root1eq1  23423  cxpeq  23425  ang180lem1  23466  ang180lem3  23468  ang180lem4  23469  1cubrlem  23495  1cubr  23496  quart1lem  23509  asin1  23548  atanlogsublem  23569  log2ublem2  23601  log2ublem3  23602  log2ub  23603  bclbnd  23934  bposlem8  23945  bposlem9  23946  lgsdir2lem5  23981  ax5seglem7  24642  ip0i  26140  ip1ilem  26141  ipasslem10  26154  siilem1  26166  normlem0  26426  normlem1  26427  normlem2  26428  normlem3  26429  normlem5  26431  normlem7  26433  bcseqi  26437  norm-ii-i  26454  normpar2i  26473  polid2i  26474  h1de2i  26871  lnopunilem1  27328  lnophmlem2  27335  ballotth  28968  problem2  29859  problem4  29861  quad3  29863  logi  29930  heiborlem6  31574  proot1ex  35505  areaquad  35528  coskpi2  37015  cosnegpi  37016  cosknegpi  37018  wallispilem4  37199  dirkerper  37227  dirkertrigeq  37232  dirkercncflem2  37235  fourierdlem57  37295  fourierdlem62  37300  fourierswlem  37362  3exp4mod41  37843  41prothprmlem1  37844  zlmodzxzequap  38592  nn0sumshdiglemB  38732  i2linesi  38818
  Copyright terms: Public domain W3C validator