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

Theorem mulcli 9383
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 9358 . 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 1756  (class class class)co 6086   CCcc 9272    x. cmul 9279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9336
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mul02lem2  9538  addid1  9541  cnegex2  9543  ixi  9957  2mulicn  10540  numma  10778  nummac  10779  decbin2  10851  irec  11957  binom2i  11967  binom2aiOLD  11968  crreczi  11981  nn0opthi  12040  faclbnd4lem1  12061  rei  12637  imi  12638  iseraltlem2  13152  odd2np1  13584  gcdaddmlem  13704  modxai  14089  mod2xnegi  14092  decexp2  14096  decsplit  14104  karatsuba  14105  sinhalfpilem  21905  ef2pi  21919  ef2kpi  21920  efper  21921  sinperlem  21922  sin2kpi  21925  cos2kpi  21926  sin2pim  21927  cos2pim  21928  sincos4thpi  21955  sincos6thpi  21957  pige3  21959  abssinper  21960  efeq1  21965  logneg  22016  logm1  22017  eflogeq  22030  logimul  22043  logneg2  22044  cxpsqr  22128  root1eq1  22173  cxpeq  22175  ang180lem1  22185  ang180lem3  22187  ang180lem4  22188  1cubrlem  22216  1cubr  22217  quart1lem  22230  asin1  22269  atanlogsublem  22290  log2ublem2  22322  log2ublem3  22323  log2ub  22324  bclbnd  22599  bposlem8  22610  bposlem9  22611  lgsdir2lem5  22646  ax5seglem7  23149  ip0i  24193  ip1ilem  24194  ipasslem10  24207  siilem1  24219  normlem0  24479  normlem1  24480  normlem2  24481  normlem3  24482  normlem5  24484  normlem7  24486  bcseqi  24490  norm-ii-i  24507  normpar2i  24526  polid2i  24527  h1de2i  24924  lnopunilem1  25382  lnophmlem2  25389  ballotth  26889  problem2  27268  problem4  27270  quad3  27272  bpoly3  28170  bpoly4  28171  heiborlem6  28686  proot1ex  29540  areaquad  29563  wallispilem4  29834  zlmodzxzequap  30972  i2linesi  31059
  Copyright terms: Public domain W3C validator