Theorem mulcli 10913

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

Syntax hints:   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   · cmul 10807

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

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

This theorem is referenced by:  mul02lem2  11082  addid1  11085  cnegex2  11087  ixi  11534  2mulicn  12126  numma  12410  nummac  12411  9t11e99  12496  decbin2  12507  irec  13846  binom2i  13856  crreczi  13871  3dec  13908  nn0opthi  13912  faclbnd4lem1  13935  rei  14795  imi  14796  iseraltlem2  15322  bpoly3  15696  bpoly4  15697  3dvdsdec  15969  3dvds2dec  15970  odd2np1  15978  gcdaddmlem  16159  3lcm2e6woprm  16248  6lcm4e12  16249  modxai  16697  mod2xnegi  16700  decexp2  16704  karatsuba  16713  sinhalfpilem  25525  ef2pi  25539  ef2kpi  25540  efper  25541  sinperlem  25542  sin2kpi  25545  cos2kpi  25546  sin2pim  25547  cos2pim  25548  sincos4thpi  25575  sincos6thpi  25577  pige3ALT  25581  abssinper  25582  efeq1  25589  logneg  25648  logm1  25649  eflogeq  25662  logimul  25674  logneg2  25675  cxpsqrt  25763  root1eq1  25813  cxpeq  25815  ang180lem1  25864  ang180lem3  25866  ang180lem4  25867  1cubrlem  25896  1cubr  25897  quart1lem  25910  asin1  25949  atanlogsublem  25970  log2ublem2  26002  log2ublem3  26003  log2ub  26004  bclbnd  26333  bposlem8  26344  bposlem9  26345  lgsdir2lem5  26382  2lgsoddprmlem3c  26465  2lgsoddprmlem3d  26466  ax5seglem7  27206  ip0i  29088  ip1ilem  29089  ipasslem10  29102  siilem1  29114  normlem0  29372  normlem1  29373  normlem2  29374  normlem3  29375  normlem5  29377  normlem7  29379  bcseqi  29383  norm-ii-i  29400  normpar2i  29419  polid2i  29420  h1de2i  29816  lnopunilem1  30273  lnophmlem2  30280  dfdec100  31046  dpmul100  31073  dp3mul10  31074  dpmul1000  31075  dpexpp1  31084  dpmul  31089  dpmul4  31090  ballotth  32404  efmul2picn  32476  itgexpif  32486  vtscl  32518  circlemeth  32520  hgt750lem  32531  problem2  33524  problem4  33526  quad3  33528  logi  33606  heiborlem6  35901  gcdaddmzz2nncomi  39932  sn-1ne2  40216  sqsumi  40230  sqmid3api  40232  sqdeccom12  40238  re1m1e0m0  40301  reixi  40325  sn-1ticom  40337  sn-0tie0  40342  sn-inelr  40356  proot1ex  40942  areaquad  40963  resqrtvalex  41142  imsqrtvalex  41143  coskpi2  43297  cosnegpi  43298  cosknegpi  43300  wallispilem4  43499  dirkerper  43527  dirkertrigeq  43532  dirkercncflem2  43535  fourierdlem57  43594  fourierdlem62  43599  fourierswlem  43661  fmtnorec3  44888  fmtnorec4  44889  lighneallem3  44947  3exp4mod41  44956  41prothprmlem1  44957  zlmodzxzequap  45728  nn0sumshdiglemB  45854  i2linesi  46368