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

Theorem mulcli 9902
Description: Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1 𝐴 ∈ ℂ
axi.2 𝐵 ∈ ℂ
Assertion
Ref Expression
mulcli (𝐴 · 𝐵) ∈ ℂ

Proof of Theorem mulcli
StepHypRef Expression
1 axi.1 . 2 𝐴 ∈ ℂ
2 axi.2 . 2 𝐵 ∈ ℂ
3 mulcl 9877 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3mp2an 703 1 (𝐴 · 𝐵) ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  (class class class)co 6527  cc 9791   · cmul 9798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 9855
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  mul02lem2  10065  addid1  10068  cnegex2  10070  ixi  10508  2mulicn  11105  numma  11392  nummac  11393  9t11e99  11506  9t11e99OLD  11507  decbin2  11518  irec  12784  binom2i  12794  crreczi  12809  3dec  12870  sq10OLD  12871  3decOLD  12873  nn0opthi  12877  faclbnd4lem1  12900  rei  13693  imi  13694  iseraltlem2  14210  bpoly3  14577  bpoly4  14578  3dvdsdec  14841  3dvdsdecOLD  14842  3dvds2dec  14843  3dvds2decOLD  14844  odd2np1  14852  gcdaddmlem  15032  3lcm2e6woprm  15115  6lcm4e12  15116  modxai  15559  mod2xnegi  15562  decexp2  15566  decsplitOLD  15578  karatsuba  15579  karatsubaOLD  15580  sinhalfpilem  23964  ef2pi  23978  ef2kpi  23979  efper  23980  sinperlem  23981  sin2kpi  23984  cos2kpi  23985  sin2pim  23986  cos2pim  23987  sincos4thpi  24014  sincos6thpi  24016  pige3  24018  abssinper  24019  efeq1  24024  logneg  24083  logm1  24084  eflogeq  24097  logimul  24109  logneg2  24110  cxpsqrt  24194  root1eq1  24241  cxpeq  24243  ang180lem1  24284  ang180lem3  24286  ang180lem4  24287  1cubrlem  24313  1cubr  24314  quart1lem  24327  asin1  24366  atanlogsublem  24387  log2ublem2  24419  log2ublem3  24420  log2ub  24421  bclbnd  24750  bposlem8  24761  bposlem9  24762  lgsdir2lem5  24799  2lgsoddprmlem3c  24882  2lgsoddprmlem3d  24883  ax5seglem7  25561  ip0i  26898  ip1ilem  26899  ipasslem10  26912  siilem1  26924  normlem0  27184  normlem1  27185  normlem2  27186  normlem3  27187  normlem5  27189  normlem7  27191  bcseqi  27195  norm-ii-i  27212  normpar2i  27231  polid2i  27232  h1de2i  27630  lnopunilem1  28087  lnophmlem2  28094  ballotth  29760  problem2  30647  problem2OLD  30648  problem4  30650  quad3  30652  logi  30707  heiborlem6  32609  proot1ex  36622  areaquad  36645  coskpi2  38573  cosnegpi  38574  cosknegpi  38576  wallispilem4  38785  dirkerper  38813  dirkertrigeq  38818  dirkercncflem2  38821  fourierdlem57  38880  fourierdlem62  38885  fourierswlem  38947  fmtnorec3  39823  fmtnorec4  39824  lighneallem3  39887  3exp4mod41  39896  41prothprmlem1  39897  zlmodzxzequap  42104  nn0sumshdiglemB  42234  i2linesi  42316
  Copyright terms: Public domain W3C validator