Theorem mulcli 10650

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537   · cmul 10544

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  mul02lem2  10819  addid1  10822  cnegex2  10824  ixi  11271  2mulicn  11863  numma  12145  nummac  12146  9t11e99  12231  decbin2  12242  irec  13567  binom2i  13577  crreczi  13592  3dec  13629  nn0opthi  13633  faclbnd4lem1  13656  rei  14517  imi  14518  iseraltlem2  15041  bpoly3  15414  bpoly4  15415  3dvdsdec  15683  3dvds2dec  15684  odd2np1  15692  gcdaddmlem  15874  3lcm2e6woprm  15961  6lcm4e12  15962  modxai  16406  mod2xnegi  16409  decexp2  16413  karatsuba  16422  sinhalfpilem  25051  ef2pi  25065  ef2kpi  25066  efper  25067  sinperlem  25068  sin2kpi  25071  cos2kpi  25072  sin2pim  25073  cos2pim  25074  sincos4thpi  25101  sincos6thpi  25103  pige3ALT  25107  abssinper  25108  efeq1  25115  logneg  25173  logm1  25174  eflogeq  25187  logimul  25199  logneg2  25200  cxpsqrt  25288  root1eq1  25338  cxpeq  25340  ang180lem1  25389  ang180lem3  25391  ang180lem4  25392  1cubrlem  25421  1cubr  25422  quart1lem  25435  asin1  25474  atanlogsublem  25495  log2ublem2  25527  log2ublem3  25528  log2ub  25529  bclbnd  25858  bposlem8  25869  bposlem9  25870  lgsdir2lem5  25907  2lgsoddprmlem3c  25990  2lgsoddprmlem3d  25991  ax5seglem7  26723  ip0i  28604  ip1ilem  28605  ipasslem10  28618  siilem1  28630  normlem0  28888  normlem1  28889  normlem2  28890  normlem3  28891  normlem5  28893  normlem7  28895  bcseqi  28899  norm-ii-i  28916  normpar2i  28935  polid2i  28936  h1de2i  29332  lnopunilem1  29789  lnophmlem2  29796  dfdec100  30548  dpmul100  30575  dp3mul10  30576  dpmul1000  30577  dpexpp1  30586  dpmul  30591  dpmul4  30592  ballotth  31797  efmul2picn  31869  itgexpif  31879  vtscl  31911  circlemeth  31913  hgt750lem  31924  problem2  32911  problem4  32913  quad3  32915  logi  32968  heiborlem6  35096  sn-1ne2  39165  sqsumi  39174  sqmid3api  39176  sqdeccom12  39182  re1m1e0m0  39234  proot1ex  39808  areaquad  39830  coskpi2  42154  cosnegpi  42155  cosknegpi  42157  wallispilem4  42360  dirkerper  42388  dirkertrigeq  42393  dirkercncflem2  42396  fourierdlem57  42455  fourierdlem62  42460  fourierswlem  42522  fmtnorec3  43717  fmtnorec4  43718  lighneallem3  43779  3exp4mod41  43788  41prothprmlem1  43789  zlmodzxzequap  44561  nn0sumshdiglemB  44687  i2linesi  44886