Theorem mulcli 11157

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   · cmul 11049

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

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

This theorem is referenced by:  mul02lem2  11327  addrid  11330  cnegex2  11332  ixi  11783  2mulicn  12382  numma  12669  nummac  12670  9t11e99  12755  decbin2  12766  irec  14142  binom2i  14153  crreczi  14169  3dec  14207  nn0opthi  14211  faclbnd4lem1  14234  rei  15098  imi  15099  iseraltlem2  15625  bpoly3  16000  bpoly4  16001  3dvdsdec  16278  3dvds2dec  16279  odd2np1  16287  gcdaddmlem  16470  3lcm2e6woprm  16561  6lcm4e12  16562  modxai  17015  mod2xnegi  17018  karatsuba  17030  sinhalfpilem  26405  ef2pi  26419  ef2kpi  26420  efper  26421  sinperlem  26422  sin2kpi  26425  cos2kpi  26426  sin2pim  26427  cos2pim  26428  sincos4thpi  26455  sincos6thpi  26458  pige3ALT  26462  abssinper  26463  efeq1  26470  logi  26529  logneg  26530  logm1  26531  eflogeq  26544  logimul  26556  logneg2  26557  cxpsqrt  26645  root1eq1  26698  cxpeq  26700  ang180lem1  26752  ang180lem3  26754  ang180lem4  26755  1cubrlem  26784  1cubr  26785  quart1lem  26798  asin1  26837  atanlogsublem  26858  log2ublem2  26890  log2ublem3  26891  log2ub  26892  bclbnd  27224  bposlem8  27235  bposlem9  27236  lgsdir2lem5  27273  2lgsoddprmlem3c  27356  2lgsoddprmlem3d  27357  ax5seglem7  28915  ip0i  30804  ip1ilem  30805  ipasslem10  30818  siilem1  30830  normlem0  31088  normlem1  31089  normlem2  31090  normlem3  31091  normlem5  31093  normlem7  31095  bcseqi  31099  norm-ii-i  31116  normpar2i  31135  polid2i  31136  h1de2i  31532  lnopunilem1  31989  lnophmlem2  31996  dfdec100  32805  dpmul100  32867  dp3mul10  32868  dpmul1000  32869  dpexpp1  32878  dpmul  32883  dpmul4  32884  cos9thpiminplylem4  33768  cos9thpiminplylem5  33769  ballotth  34522  efmul2picn  34580  itgexpif  34590  vtscl  34622  circlemeth  34624  hgt750lem  34635  problem2  35646  problem4  35648  quad3  35650  heiborlem6  37803  gcdaddmzz2nncomi  41976  sn-1ne2  42246  sqsumi  42262  sqmid3api  42264  sqdeccom12  42270  cxp112d  42322  cxp111d  42323  cxpi11d  42324  re1m1e0m0  42378  reixi  42404  sn-1ticom  42416  sn-0tie0  42432  proot1ex  43178  areaquad  43198  resqrtvalex  43627  imsqrtvalex  43628  coskpi2  45857  cosnegpi  45858  cosknegpi  45860  wallispilem4  46059  dirkerper  46087  dirkertrigeq  46092  dirkercncflem2  46095  fourierdlem57  46154  fourierdlem62  46159  fourierswlem  46221  fmtnorec3  47542  fmtnorec4  47543  lighneallem3  47601  3exp4mod41  47610  41prothprmlem1  47611  zlmodzxzequap  48481  nn0sumshdiglemB  48602  i2linesi  49760