Theorem mulcli 11151

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   · cmul 11043

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

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

This theorem is referenced by:  mul02lem2  11322  addrid  11325  cnegex2  11327  ixi  11778  2mulicn  12377  numma  12663  nummac  12664  9t11e99  12749  decbin2  12760  irec  14136  binom2i  14147  crreczi  14163  3dec  14201  nn0opthi  14205  faclbnd4lem1  14228  rei  15091  imi  15092  iseraltlem2  15618  bpoly3  15993  bpoly4  15994  3dvdsdec  16271  3dvds2dec  16272  odd2np1  16280  gcdaddmlem  16463  3lcm2e6woprm  16554  6lcm4e12  16555  modxai  17008  mod2xnegi  17011  karatsuba  17023  sinhalfpilem  26443  ef2pi  26457  ef2kpi  26458  efper  26459  sinperlem  26460  sin2kpi  26463  cos2kpi  26464  sin2pim  26465  cos2pim  26466  sincos4thpi  26493  sincos6thpi  26496  pige3ALT  26500  abssinper  26501  efeq1  26508  logi  26567  logneg  26568  logm1  26569  eflogeq  26582  logimul  26594  logneg2  26595  cxpsqrt  26683  root1eq1  26736  cxpeq  26738  ang180lem1  26790  ang180lem3  26792  ang180lem4  26793  1cubrlem  26822  1cubr  26823  quart1lem  26836  asin1  26875  atanlogsublem  26896  log2ublem2  26928  log2ublem3  26929  log2ub  26930  bclbnd  27262  bposlem8  27273  bposlem9  27274  lgsdir2lem5  27311  2lgsoddprmlem3c  27394  2lgsoddprmlem3d  27395  ax5seglem7  29024  ip0i  30917  ip1ilem  30918  ipasslem10  30931  siilem1  30943  normlem0  31201  normlem1  31202  normlem2  31203  normlem3  31204  normlem5  31206  normlem7  31208  bcseqi  31212  norm-ii-i  31229  normpar2i  31248  polid2i  31249  h1de2i  31645  lnopunilem1  32102  lnophmlem2  32109  dfdec100  32926  dpmul100  32993  dp3mul10  32994  dpmul1000  32995  dpexpp1  33004  dpmul  33009  dpmul4  33010  cos9thpiminplylem4  33967  cos9thpiminplylem5  33968  ballotth  34720  efmul2picn  34778  itgexpif  34788  vtscl  34820  circlemeth  34822  hgt750lem  34833  problem2  35886  problem4  35888  quad3  35890  heiborlem6  38071  gcdaddmzz2nncomi  42369  sn-1ne2  42639  sqsumi  42655  sqmid3api  42657  sqdeccom12  42663  cxp112d  42715  cxp111d  42716  cxpi11d  42717  re1m1e0m0  42771  reixi  42797  sn-1ticom  42809  sn-0tie0  42825  proot1ex  43557  areaquad  43577  resqrtvalex  44005  imsqrtvalex  44006  coskpi2  46228  cosnegpi  46229  cosknegpi  46231  wallispilem4  46430  dirkerper  46458  dirkertrigeq  46463  dirkercncflem2  46466  fourierdlem57  46525  fourierdlem62  46530  fourierswlem  46592  fmtnorec3  47912  fmtnorec4  47913  lighneallem3  47971  3exp4mod41  47980  41prothprmlem1  47981  zlmodzxzequap  48863  nn0sumshdiglemB  48984  i2linesi  50141