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

Theorem mulcli 9597
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 9572 . 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 1767  (class class class)co 6282   CCcc 9486    x. cmul 9493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9550
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul02lem2  9752  addid1  9755  cnegex2  9757  ixi  10174  2mulicn  10758  numma  11003  nummac  11004  decbin2  11076  irec  12229  binom2i  12239  binom2aiOLD  12240  crreczi  12253  nn0opthi  12312  faclbnd4lem1  12333  rei  12946  imi  12947  iseraltlem2  13461  odd2np1  13898  gcdaddmlem  14018  modxai  14406  mod2xnegi  14409  decexp2  14413  decsplit  14421  karatsuba  14422  sinhalfpilem  22586  ef2pi  22600  ef2kpi  22601  efper  22602  sinperlem  22603  sin2kpi  22606  cos2kpi  22607  sin2pim  22608  cos2pim  22609  sincos4thpi  22636  sincos6thpi  22638  pige3  22640  abssinper  22641  efeq1  22646  logneg  22697  logm1  22698  eflogeq  22711  logimul  22724  logneg2  22725  cxpsqrt  22809  root1eq1  22854  cxpeq  22856  ang180lem1  22866  ang180lem3  22868  ang180lem4  22869  1cubrlem  22897  1cubr  22898  quart1lem  22911  asin1  22950  atanlogsublem  22971  log2ublem2  23003  log2ublem3  23004  log2ub  23005  bclbnd  23280  bposlem8  23291  bposlem9  23292  lgsdir2lem5  23327  ax5seglem7  23911  ip0i  25413  ip1ilem  25414  ipasslem10  25427  siilem1  25439  normlem0  25699  normlem1  25700  normlem2  25701  normlem3  25702  normlem5  25704  normlem7  25706  bcseqi  25710  norm-ii-i  25727  normpar2i  25746  polid2i  25747  h1de2i  26144  lnopunilem1  26602  lnophmlem2  26609  ballotth  28113  problem2  28492  problem4  28494  quad3  28496  bpoly3  29394  bpoly4  29395  heiborlem6  29913  proot1ex  30766  areaquad  30789  coskpi2  31202  cosnegpi  31203  cosknegpi  31205  wallispilem4  31368  dirkerper  31396  dirkertrigeq  31401  dirkercncflem2  31404  fourierdlem57  31464  fourierdlem62  31469  fourierswlem  31531  zlmodzxzequap  32181  i2linesi  32274
  Copyright terms: Public domain W3C validator