Theorem mulcli 11119

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

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		mulcl 11090	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 · 𝐵) ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004   · cmul 11011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 11068

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mul02lem2  11290  addrid  11293  cnegex2  11295  ixi  11746  2mulicn  12345  numma  12632  nummac  12633  9t11e99  12718  decbin2  12729  irec  14108  binom2i  14119  crreczi  14135  3dec  14173  nn0opthi  14177  faclbnd4lem1  14200  rei  15063  imi  15064  iseraltlem2  15590  bpoly3  15965  bpoly4  15966  3dvdsdec  16243  3dvds2dec  16244  odd2np1  16252  gcdaddmlem  16435  3lcm2e6woprm  16526  6lcm4e12  16527  modxai  16980  mod2xnegi  16983  karatsuba  16995  sinhalfpilem  26399  ef2pi  26413  ef2kpi  26414  efper  26415  sinperlem  26416  sin2kpi  26419  cos2kpi  26420  sin2pim  26421  cos2pim  26422  sincos4thpi  26449  sincos6thpi  26452  pige3ALT  26456  abssinper  26457  efeq1  26464  logi  26523  logneg  26524  logm1  26525  eflogeq  26538  logimul  26550  logneg2  26551  cxpsqrt  26639  root1eq1  26692  cxpeq  26694  ang180lem1  26746  ang180lem3  26748  ang180lem4  26749  1cubrlem  26778  1cubr  26779  quart1lem  26792  asin1  26831  atanlogsublem  26852  log2ublem2  26884  log2ublem3  26885  log2ub  26886  bclbnd  27218  bposlem8  27229  bposlem9  27230  lgsdir2lem5  27267  2lgsoddprmlem3c  27350  2lgsoddprmlem3d  27351  ax5seglem7  28913  ip0i  30805  ip1ilem  30806  ipasslem10  30819  siilem1  30831  normlem0  31089  normlem1  31090  normlem2  31091  normlem3  31092  normlem5  31094  normlem7  31096  bcseqi  31100  norm-ii-i  31117  normpar2i  31136  polid2i  31137  h1de2i  31533  lnopunilem1  31990  lnophmlem2  31997  dfdec100  32813  dpmul100  32877  dp3mul10  32878  dpmul1000  32879  dpexpp1  32888  dpmul  32893  dpmul4  32894  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  ballotth  34551  efmul2picn  34609  itgexpif  34619  vtscl  34651  circlemeth  34653  hgt750lem  34664  problem2  35710  problem4  35712  quad3  35714  heiborlem6  37866  gcdaddmzz2nncomi  42098  sn-1ne2  42368  sqsumi  42384  sqmid3api  42386  sqdeccom12  42392  cxp112d  42444  cxp111d  42445  cxpi11d  42446  re1m1e0m0  42500  reixi  42526  sn-1ticom  42538  sn-0tie0  42554  proot1ex  43299  areaquad  43319  resqrtvalex  43748  imsqrtvalex  43749  coskpi2  45974  cosnegpi  45975  cosknegpi  45977  wallispilem4  46176  dirkerper  46204  dirkertrigeq  46209  dirkercncflem2  46212  fourierdlem57  46271  fourierdlem62  46276  fourierswlem  46338  fmtnorec3  47658  fmtnorec4  47659  lighneallem3  47717  3exp4mod41  47726  41prothprmlem1  47727  zlmodzxzequap  48610  nn0sumshdiglemB  48731  i2linesi  49889