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

Theorem mulcli 9055
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 9034 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3mp2an 654 1  |-  ( A  x.  B )  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1721  (class class class)co 6044   CCcc 8948    x. cmul 8955
This theorem is referenced by:  mul02lem2  9203  addid1  9206  cnegex2  9208  ixi  9611  numma  10373  nummac  10374  decbin2  10446  irec  11439  binom2i  11449  binom2aiOLD  11450  crreczi  11463  nn0opthi  11522  faclbnd4lem1  11543  imval2  11915  rei  11920  imi  11921  iseraltlem2  12435  sinf  12684  sinneg  12706  efival  12712  sinadd  12724  odd2np1  12867  gcdaddmlem  12987  modxai  13363  mod2xnegi  13366  decexp2  13370  decsplit  13378  karatsuba  13379  dvmptim  19813  sincn  20317  sinhalfpilem  20331  ef2pi  20342  ef2kpi  20343  efper  20344  sinperlem  20345  sin2kpi  20348  cos2kpi  20349  sin2pim  20350  cos2pim  20351  sincos4thpi  20378  sincos6thpi  20380  pige3  20382  abssinper  20383  sineq0  20386  efeq1  20388  logneg  20439  logm1  20440  eflogeq  20453  logimul  20466  logneg2  20467  cxpsqr  20551  root1eq1  20596  cxpeq  20598  ang180lem1  20608  ang180lem3  20610  ang180lem4  20611  1cubrlem  20638  1cubr  20639  quart1lem  20652  sinasin  20686  asin1  20691  atanlogsublem  20712  efiatan2  20714  2efiatan  20715  tanatan  20716  log2ublem2  20744  log2ublem3  20745  log2ub  20746  bclbnd  21021  bposlem8  21032  bposlem9  21033  lgsdir2lem5  21068  ip0i  22283  ip1ilem  22284  ipasslem10  22297  siilem1  22309  normlem0  22568  normlem1  22569  normlem2  22570  normlem3  22571  normlem5  22573  normlem7  22575  bcseqi  22579  norm-ii-i  22596  normpar2i  22615  polid2i  22616  h1de2i  23012  lnopunilem1  23470  lnophmlem2  23477  ballotth  24752  ax5seglem7  25782  bpoly3  26012  bpoly4  26013  heiborlem6  26419  proot1ex  27392  wallispilem4  27688
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcl 9012
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator