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

Theorem mulcli 8842
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 8821 . 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 1684  (class class class)co 5858   CCcc 8735    x. cmul 8742
This theorem is referenced by:  mul02lem2  8989  addid1  8992  cnegex2  8994  ixi  9397  numma  10155  nummac  10156  decbin2  10228  irec  11202  binom2i  11212  binom2aiOLD  11213  crreczi  11226  nn0opthi  11285  faclbnd4lem1  11306  imval2  11636  rei  11641  imi  11642  iseraltlem2  12155  sinf  12404  sinneg  12426  efival  12432  sinadd  12444  odd2np1  12587  gcdaddmlem  12707  modxai  13083  mod2xnegi  13086  decexp2  13090  decsplit  13098  karatsuba  13099  dvmptim  19319  sincn  19820  sinhalfpilem  19834  ef2pi  19845  ef2kpi  19846  efper  19847  sinperlem  19848  sin2kpi  19851  cos2kpi  19852  sin2pim  19853  cos2pim  19854  sincos4thpi  19881  sincos6thpi  19883  pige3  19885  abssinper  19886  sineq0  19889  efeq1  19891  logneg  19941  logm1  19942  eflogeq  19955  logimul  19968  logneg2  19969  cxpsqr  20050  root1eq1  20095  cxpeq  20097  ang180lem1  20107  ang180lem3  20109  ang180lem4  20110  1cubrlem  20137  1cubr  20138  quart1lem  20151  sinasin  20185  asin1  20190  atanlogsublem  20211  efiatan2  20213  2efiatan  20214  tanatan  20215  log2ublem2  20243  log2ublem3  20244  log2ub  20245  bclbnd  20519  bposlem8  20530  bposlem9  20531  lgsdir2lem5  20566  ip0i  21403  ip1ilem  21404  ipasslem10  21417  siilem1  21429  normlem0  21688  normlem1  21689  normlem2  21690  normlem3  21691  normlem5  21693  normlem7  21695  bcseqi  21699  norm-ii-i  21716  normpar2i  21735  polid2i  21736  h1de2i  22132  lnopunilem1  22590  lnophmlem2  22597  ballotth  23096  ax5seglem7  24563  bpoly3  24793  bpoly4  24794  cnegvex2  25660  heiborlem6  26540  proot1ex  27520  wallispilem4  27817
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcl 8799
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator