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

Theorem mulcli 8989
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 8968 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3mp2an 653 1  |-  ( A  x.  B )  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1715  (class class class)co 5981   CCcc 8882    x. cmul 8889
This theorem is referenced by:  mul02lem2  9136  addid1  9139  cnegex2  9141  ixi  9544  numma  10306  nummac  10307  decbin2  10379  irec  11367  binom2i  11377  binom2aiOLD  11378  crreczi  11391  nn0opthi  11450  faclbnd4lem1  11471  imval2  11843  rei  11848  imi  11849  iseraltlem2  12363  sinf  12612  sinneg  12634  efival  12640  sinadd  12652  odd2np1  12795  gcdaddmlem  12915  modxai  13291  mod2xnegi  13294  decexp2  13298  decsplit  13306  karatsuba  13307  dvmptim  19534  sincn  20038  sinhalfpilem  20052  ef2pi  20063  ef2kpi  20064  efper  20065  sinperlem  20066  sin2kpi  20069  cos2kpi  20070  sin2pim  20071  cos2pim  20072  sincos4thpi  20099  sincos6thpi  20101  pige3  20103  abssinper  20104  sineq0  20107  efeq1  20109  logneg  20160  logm1  20161  eflogeq  20174  logimul  20187  logneg2  20188  cxpsqr  20272  root1eq1  20317  cxpeq  20319  ang180lem1  20329  ang180lem3  20331  ang180lem4  20332  1cubrlem  20359  1cubr  20360  quart1lem  20373  sinasin  20407  asin1  20412  atanlogsublem  20433  efiatan2  20435  2efiatan  20436  tanatan  20437  log2ublem2  20465  log2ublem3  20466  log2ub  20467  bclbnd  20742  bposlem8  20753  bposlem9  20754  lgsdir2lem5  20789  ip0i  21716  ip1ilem  21717  ipasslem10  21730  siilem1  21742  normlem0  22001  normlem1  22002  normlem2  22003  normlem3  22004  normlem5  22006  normlem7  22008  bcseqi  22012  norm-ii-i  22029  normpar2i  22048  polid2i  22049  h1de2i  22445  lnopunilem1  22903  lnophmlem2  22910  ballotth  24243  ax5seglem7  25305  bpoly3  25535  bpoly4  25536  heiborlem6  26046  proot1ex  27026  wallispilem4  27323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcl 8946
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator