Theorem mulcli 11143

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

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027   · cmul 11034

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

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  mul02lem2  11314  addrid  11317  cnegex2  11319  ixi  11770  2mulicn  12392  numma  12679  nummac  12680  9t11e99  12765  decbin2  12776  irec  14154  binom2i  14165  crreczi  14181  3dec  14219  nn0opthi  14223  faclbnd4lem1  14246  rei  15109  imi  15110  iseraltlem2  15636  bpoly3  16014  bpoly4  16015  3dvdsdec  16292  3dvds2dec  16293  odd2np1  16301  gcdaddmlem  16484  3lcm2e6woprm  16575  6lcm4e12  16576  modxai  17030  mod2xnegi  17033  karatsuba  17045  sinhalfpilem  26445  ef2pi  26459  ef2kpi  26460  efper  26461  sinperlem  26462  sin2kpi  26465  cos2kpi  26466  sin2pim  26467  cos2pim  26468  sincos4thpi  26495  sincos6thpi  26498  pige3ALT  26502  abssinper  26503  efeq1  26510  logi  26569  logneg  26570  logm1  26571  eflogeq  26584  logimul  26596  logneg2  26597  cxpsqrt  26685  root1eq1  26737  cxpeq  26739  ang180lem1  26791  ang180lem3  26793  ang180lem4  26794  1cubrlem  26823  1cubr  26824  quart1lem  26837  asin1  26876  atanlogsublem  26897  log2ublem2  26929  log2ublem3  26930  log2ub  26931  bclbnd  27261  bposlem8  27272  bposlem9  27273  lgsdir2lem5  27310  2lgsoddprmlem3c  27393  2lgsoddprmlem3d  27394  ax5seglem7  29022  ip0i  30914  ip1ilem  30915  ipasslem10  30928  siilem1  30940  normlem0  31198  normlem1  31199  normlem2  31200  normlem3  31201  normlem5  31203  normlem7  31205  bcseqi  31209  norm-ii-i  31226  normpar2i  31245  polid2i  31246  h1de2i  31642  lnopunilem1  32099  lnophmlem2  32106  dfdec100  32922  dpmul100  32975  dp3mul10  32976  dpmul1000  32977  dpexpp1  32986  dpmul  32991  dpmul4  32992  cos9thpiminplylem4  33969  cos9thpiminplylem5  33970  ballotth  34722  efmul2picn  34780  itgexpif  34790  vtscl  34822  circlemeth  34824  hgt750lem  34835  problem2  35894  problem4  35896  quad3  35898  heiborlem6  38183  gcdaddmzz2nncomi  42480  sn-1ne2  42748  sqsumi  42758  sqmid3api  42760  sqdeccom12  42766  cxp112d  42818  cxp111d  42819  cxpi11d  42820  re1m1e0m0  42874  reixi  42900  sn-1ticom  42912  sn-0tie0  42941  proot1ex  43641  areaquad  43661  resqrtvalex  44089  imsqrtvalex  44090  coskpi2  46309  cosnegpi  46310  cosknegpi  46312  wallispilem4  46511  dirkerper  46539  dirkertrigeq  46544  dirkercncflem2  46547  fourierdlem57  46606  fourierdlem62  46611  fourierswlem  46673  cos5t  47342  goldrasin  47345  fmtnorec3  48026  fmtnorec4  48027  lighneallem3  48085  3exp4mod41  48094  41prothprmlem1  48095  zlmodzxzequap  48990  nn0sumshdiglemB  49111  i2linesi  50268