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

Theorem mulcli 10083
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 10058 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
41, 2, 3mp2an 708 1 (𝐴 · 𝐵) ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  (class class class)co 6690  cc 9972   · cmul 9979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 10036
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  mul02lem2  10251  addid1  10254  cnegex2  10256  ixi  10694  2mulicn  11293  numma  11595  nummac  11596  9t11e99  11709  9t11e99OLD  11710  decbin2  11721  irec  13004  binom2i  13014  crreczi  13029  3dec  13090  sq10OLD  13091  3decOLD  13093  nn0opthi  13097  faclbnd4lem1  13120  rei  13940  imi  13941  iseraltlem2  14457  bpoly3  14833  bpoly4  14834  3dvdsdec  15101  3dvdsdecOLD  15102  3dvds2dec  15103  3dvds2decOLD  15104  odd2np1  15112  gcdaddmlem  15292  3lcm2e6woprm  15375  6lcm4e12  15376  modxai  15819  mod2xnegi  15822  decexp2  15826  decsplitOLD  15838  karatsuba  15839  karatsubaOLD  15840  sinhalfpilem  24260  ef2pi  24274  ef2kpi  24275  efper  24276  sinperlem  24277  sin2kpi  24280  cos2kpi  24281  sin2pim  24282  cos2pim  24283  sincos4thpi  24310  sincos6thpi  24312  pige3  24314  abssinper  24315  efeq1  24320  logneg  24379  logm1  24380  eflogeq  24393  logimul  24405  logneg2  24406  cxpsqrt  24494  root1eq1  24541  cxpeq  24543  ang180lem1  24584  ang180lem3  24586  ang180lem4  24587  1cubrlem  24613  1cubr  24614  quart1lem  24627  asin1  24666  atanlogsublem  24687  log2ublem2  24719  log2ublem3  24720  log2ub  24721  bclbnd  25050  bposlem8  25061  bposlem9  25062  lgsdir2lem5  25099  2lgsoddprmlem3c  25182  2lgsoddprmlem3d  25183  ax5seglem7  25860  ip0i  27808  ip1ilem  27809  ipasslem10  27822  siilem1  27834  normlem0  28094  normlem1  28095  normlem2  28096  normlem3  28097  normlem5  28099  normlem7  28101  bcseqi  28105  norm-ii-i  28122  normpar2i  28141  polid2i  28142  h1de2i  28540  lnopunilem1  28997  lnophmlem2  29004  dfdec100  29704  dpmul100  29733  dp3mul10  29734  dpmul1000  29735  dpexpp1  29744  dpmul  29749  dpmul4  29750  ballotth  30727  efmul2picn  30802  itgexpif  30812  vtscl  30844  circlemeth  30846  hgt750lem  30857  problem2  31685  problem2OLD  31686  problem4  31688  quad3  31690  logi  31746  heiborlem6  33745  proot1ex  38096  areaquad  38119  coskpi2  40395  cosnegpi  40396  cosknegpi  40398  wallispilem4  40603  dirkerper  40631  dirkertrigeq  40636  dirkercncflem2  40639  fourierdlem57  40698  fourierdlem62  40703  fourierswlem  40765  fmtnorec3  41785  fmtnorec4  41786  lighneallem3  41849  3exp4mod41  41858  41prothprmlem1  41859  zlmodzxzequap  42613  nn0sumshdiglemB  42739  i2linesi  42852
  Copyright terms: Public domain W3C validator