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

Theorem mulcli 9501
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 9476 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3mp2an 672 1  |-  ( A  x.  B )  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1758  (class class class)co 6199   CCcc 9390    x. cmul 9397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9454
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul02lem2  9656  addid1  9659  cnegex2  9661  ixi  10075  2mulicn  10658  numma  10896  nummac  10897  decbin2  10969  irec  12081  binom2i  12091  binom2aiOLD  12092  crreczi  12105  nn0opthi  12164  faclbnd4lem1  12185  rei  12762  imi  12763  iseraltlem2  13277  odd2np1  13709  gcdaddmlem  13829  modxai  14214  mod2xnegi  14217  decexp2  14221  decsplit  14229  karatsuba  14230  sinhalfpilem  22057  ef2pi  22071  ef2kpi  22072  efper  22073  sinperlem  22074  sin2kpi  22077  cos2kpi  22078  sin2pim  22079  cos2pim  22080  sincos4thpi  22107  sincos6thpi  22109  pige3  22111  abssinper  22112  efeq1  22117  logneg  22168  logm1  22169  eflogeq  22182  logimul  22195  logneg2  22196  cxpsqr  22280  root1eq1  22325  cxpeq  22327  ang180lem1  22337  ang180lem3  22339  ang180lem4  22340  1cubrlem  22368  1cubr  22369  quart1lem  22382  asin1  22421  atanlogsublem  22442  log2ublem2  22474  log2ublem3  22475  log2ub  22476  bclbnd  22751  bposlem8  22762  bposlem9  22763  lgsdir2lem5  22798  ax5seglem7  23332  ip0i  24376  ip1ilem  24377  ipasslem10  24390  siilem1  24402  normlem0  24662  normlem1  24663  normlem2  24664  normlem3  24665  normlem5  24667  normlem7  24669  bcseqi  24673  norm-ii-i  24690  normpar2i  24709  polid2i  24710  h1de2i  25107  lnopunilem1  25565  lnophmlem2  25572  ballotth  27063  problem2  27442  problem4  27444  quad3  27446  bpoly3  28344  bpoly4  28345  heiborlem6  28862  proot1ex  29716  areaquad  29739  wallispilem4  30010  zlmodzxzequap  31159  i2linesi  31447
  Copyright terms: Public domain W3C validator