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

Theorem mulcli 9379
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 9354 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3mp2an 665 1  |-  ( A  x.  B )  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755  (class class class)co 6080   CCcc 9268    x. cmul 9275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9332
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul02lem2  9534  addid1  9537  cnegex2  9539  ixi  9953  2mulicn  10536  numma  10774  nummac  10775  decbin2  10847  irec  11949  binom2i  11959  binom2aiOLD  11960  crreczi  11973  nn0opthi  12032  faclbnd4lem1  12053  rei  12629  imi  12630  iseraltlem2  13144  odd2np1  13575  gcdaddmlem  13695  modxai  14080  mod2xnegi  14083  decexp2  14087  decsplit  14095  karatsuba  14096  sinhalfpilem  21810  ef2pi  21824  ef2kpi  21825  efper  21826  sinperlem  21827  sin2kpi  21830  cos2kpi  21831  sin2pim  21832  cos2pim  21833  sincos4thpi  21860  sincos6thpi  21862  pige3  21864  abssinper  21865  efeq1  21870  logneg  21921  logm1  21922  eflogeq  21935  logimul  21948  logneg2  21949  cxpsqr  22033  root1eq1  22078  cxpeq  22080  ang180lem1  22090  ang180lem3  22092  ang180lem4  22093  1cubrlem  22121  1cubr  22122  quart1lem  22135  asin1  22174  atanlogsublem  22195  log2ublem2  22227  log2ublem3  22228  log2ub  22229  bclbnd  22504  bposlem8  22515  bposlem9  22516  lgsdir2lem5  22551  ax5seglem7  23004  ip0i  24048  ip1ilem  24049  ipasslem10  24062  siilem1  24074  normlem0  24334  normlem1  24335  normlem2  24336  normlem3  24337  normlem5  24339  normlem7  24341  bcseqi  24345  norm-ii-i  24362  normpar2i  24381  polid2i  24382  h1de2i  24779  lnopunilem1  25237  lnophmlem2  25244  ballotth  26768  problem2  27147  problem4  27149  bpoly3  28048  bpoly4  28049  heiborlem6  28559  proot1ex  29414  areaquad  29437  wallispilem4  29709  zlmodzxzequap  30750  i2linesi  30837
  Copyright terms: Public domain W3C validator