Theorem mulcli 11266

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 11237	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 · 𝐵) ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151   · cmul 11158

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

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

This theorem is referenced by:  mul02lem2  11436  addrid  11439  cnegex2  11441  ixi  11890  2mulicn  12487  numma  12775  nummac  12776  9t11e99  12861  decbin2  12872  irec  14237  binom2i  14248  crreczi  14264  3dec  14302  nn0opthi  14306  faclbnd4lem1  14329  rei  15192  imi  15193  iseraltlem2  15716  bpoly3  16091  bpoly4  16092  3dvdsdec  16366  3dvds2dec  16367  odd2np1  16375  gcdaddmlem  16558  3lcm2e6woprm  16649  6lcm4e12  16650  modxai  17102  mod2xnegi  17105  decexp2  17109  karatsuba  17118  sinhalfpilem  26520  ef2pi  26534  ef2kpi  26535  efper  26536  sinperlem  26537  sin2kpi  26540  cos2kpi  26541  sin2pim  26542  cos2pim  26543  sincos4thpi  26570  sincos6thpi  26573  pige3ALT  26577  abssinper  26578  efeq1  26585  logi  26644  logneg  26645  logm1  26646  eflogeq  26659  logimul  26671  logneg2  26672  cxpsqrt  26760  root1eq1  26813  cxpeq  26815  ang180lem1  26867  ang180lem3  26869  ang180lem4  26870  1cubrlem  26899  1cubr  26900  quart1lem  26913  asin1  26952  atanlogsublem  26973  log2ublem2  27005  log2ublem3  27006  log2ub  27007  bclbnd  27339  bposlem8  27350  bposlem9  27351  lgsdir2lem5  27388  2lgsoddprmlem3c  27471  2lgsoddprmlem3d  27472  ax5seglem7  28965  ip0i  30854  ip1ilem  30855  ipasslem10  30868  siilem1  30880  normlem0  31138  normlem1  31139  normlem2  31140  normlem3  31141  normlem5  31143  normlem7  31145  bcseqi  31149  norm-ii-i  31166  normpar2i  31185  polid2i  31186  h1de2i  31582  lnopunilem1  32039  lnophmlem2  32046  dfdec100  32837  dpmul100  32864  dp3mul10  32865  dpmul1000  32866  dpexpp1  32875  dpmul  32880  dpmul4  32881  ballotth  34519  efmul2picn  34590  itgexpif  34600  vtscl  34632  circlemeth  34634  hgt750lem  34645  problem2  35651  problem4  35653  quad3  35655  heiborlem6  37803  gcdaddmzz2nncomi  41977  sn-1ne2  42279  sqsumi  42295  sqmid3api  42297  sqdeccom12  42303  cxp112d  42356  cxp111d  42357  cxpi11d  42358  re1m1e0m0  42404  reixi  42429  sn-1ticom  42441  sn-0tie0  42446  sn-inelr  42474  proot1ex  43185  areaquad  43205  resqrtvalex  43635  imsqrtvalex  43636  coskpi2  45822  cosnegpi  45823  cosknegpi  45825  wallispilem4  46024  dirkerper  46052  dirkertrigeq  46057  dirkercncflem2  46060  fourierdlem57  46119  fourierdlem62  46124  fourierswlem  46186  fmtnorec3  47473  fmtnorec4  47474  lighneallem3  47532  3exp4mod41  47541  41prothprmlem1  47542  zlmodzxzequap  48345  nn0sumshdiglemB  48470  i2linesi  49009