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

Theorem mulcli 11159
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 11132 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3mp2an 690 1 (𝐴 · 𝐵) ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  (class class class)co 7354  cc 11046   · cmul 11053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 11110
This theorem depends on definitions:  df-bi 206  df-an 397
This theorem is referenced by:  mul02lem2  11329  addid1  11332  cnegex2  11334  ixi  11781  2mulicn  12373  numma  12659  nummac  12660  9t11e99  12745  decbin2  12756  irec  14102  binom2i  14113  crreczi  14128  3dec  14163  nn0opthi  14167  faclbnd4lem1  14190  rei  15038  imi  15039  iseraltlem2  15564  bpoly3  15938  bpoly4  15939  3dvdsdec  16211  3dvds2dec  16212  odd2np1  16220  gcdaddmlem  16401  3lcm2e6woprm  16488  6lcm4e12  16489  modxai  16937  mod2xnegi  16940  decexp2  16944  karatsuba  16953  sinhalfpilem  25816  ef2pi  25830  ef2kpi  25831  efper  25832  sinperlem  25833  sin2kpi  25836  cos2kpi  25837  sin2pim  25838  cos2pim  25839  sincos4thpi  25866  sincos6thpi  25868  pige3ALT  25872  abssinper  25873  efeq1  25880  logneg  25939  logm1  25940  eflogeq  25953  logimul  25965  logneg2  25966  cxpsqrt  26054  root1eq1  26104  cxpeq  26106  ang180lem1  26155  ang180lem3  26157  ang180lem4  26158  1cubrlem  26187  1cubr  26188  quart1lem  26201  asin1  26240  atanlogsublem  26261  log2ublem2  26293  log2ublem3  26294  log2ub  26295  bclbnd  26624  bposlem8  26635  bposlem9  26636  lgsdir2lem5  26673  2lgsoddprmlem3c  26756  2lgsoddprmlem3d  26757  ax5seglem7  27782  ip0i  29665  ip1ilem  29666  ipasslem10  29679  siilem1  29691  normlem0  29949  normlem1  29950  normlem2  29951  normlem3  29952  normlem5  29954  normlem7  29956  bcseqi  29960  norm-ii-i  29977  normpar2i  29996  polid2i  29997  h1de2i  30393  lnopunilem1  30850  lnophmlem2  30857  dfdec100  31621  dpmul100  31648  dp3mul10  31649  dpmul1000  31650  dpexpp1  31659  dpmul  31664  dpmul4  31665  ballotth  33028  efmul2picn  33100  itgexpif  33110  vtscl  33142  circlemeth  33144  hgt750lem  33155  problem2  34145  problem4  34147  quad3  34149  logi  34199  heiborlem6  36264  gcdaddmzz2nncomi  40442  sn-1ne2  40757  sqsumi  40771  sqmid3api  40773  sqdeccom12  40779  re1m1e0m0  40842  reixi  40867  sn-1ticom  40879  sn-0tie0  40884  sn-inelr  40910  proot1ex  41504  areaquad  41526  resqrtvalex  41897  imsqrtvalex  41898  coskpi2  44077  cosnegpi  44078  cosknegpi  44080  wallispilem4  44279  dirkerper  44307  dirkertrigeq  44312  dirkercncflem2  44315  fourierdlem57  44374  fourierdlem62  44379  fourierswlem  44441  fmtnorec3  45710  fmtnorec4  45711  lighneallem3  45769  3exp4mod41  45778  41prothprmlem1  45779  zlmodzxzequap  46550  nn0sumshdiglemB  46676  i2linesi  47195
  Copyright terms: Public domain W3C validator