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

Theorem mulcli 9100
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 9079 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  e.  CC )
41, 2, 3mp2an 655 1  |-  ( A  x.  B )  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1726  (class class class)co 6084   CCcc 8993    x. cmul 9000
This theorem is referenced by:  mul02lem2  9248  addid1  9251  cnegex2  9253  ixi  9656  numma  10418  nummac  10419  decbin2  10491  irec  11485  binom2i  11495  binom2aiOLD  11496  crreczi  11509  nn0opthi  11568  faclbnd4lem1  11589  imval2  11961  rei  11966  imi  11967  iseraltlem2  12481  sinf  12730  sinneg  12752  efival  12758  sinadd  12770  odd2np1  12913  gcdaddmlem  13033  modxai  13409  mod2xnegi  13412  decexp2  13416  decsplit  13424  karatsuba  13425  dvmptim  19861  sincn  20365  sinhalfpilem  20379  ef2pi  20390  ef2kpi  20391  efper  20392  sinperlem  20393  sin2kpi  20396  cos2kpi  20397  sin2pim  20398  cos2pim  20399  sincos4thpi  20426  sincos6thpi  20428  pige3  20430  abssinper  20431  sineq0  20434  efeq1  20436  logneg  20487  logm1  20488  eflogeq  20501  logimul  20514  logneg2  20515  cxpsqr  20599  root1eq1  20644  cxpeq  20646  ang180lem1  20656  ang180lem3  20658  ang180lem4  20659  1cubrlem  20686  1cubr  20687  quart1lem  20700  sinasin  20734  asin1  20739  atanlogsublem  20760  efiatan2  20762  2efiatan  20763  tanatan  20764  log2ublem2  20792  log2ublem3  20793  log2ub  20794  bclbnd  21069  bposlem8  21080  bposlem9  21081  lgsdir2lem5  21116  ip0i  22331  ip1ilem  22332  ipasslem10  22345  siilem1  22357  normlem0  22616  normlem1  22617  normlem2  22618  normlem3  22619  normlem5  22621  normlem7  22623  bcseqi  22627  norm-ii-i  22644  normpar2i  22663  polid2i  22664  h1de2i  23060  lnopunilem1  23518  lnophmlem2  23525  ballotth  24800  ax5seglem7  25879  bpoly3  26109  bpoly4  26110  heiborlem6  26539  proot1ex  27511  wallispilem4  27807  sineq0ALT  29123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9057
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator