Theorem mulcli 11247

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132   · cmul 11139

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

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

This theorem is referenced by:  mul02lem2  11417  addrid  11420  cnegex2  11422  ixi  11871  2mulicn  12470  numma  12757  nummac  12758  9t11e99  12843  decbin2  12854  irec  14224  binom2i  14235  crreczi  14251  3dec  14289  nn0opthi  14293  faclbnd4lem1  14316  rei  15180  imi  15181  iseraltlem2  15704  bpoly3  16079  bpoly4  16080  3dvdsdec  16356  3dvds2dec  16357  odd2np1  16365  gcdaddmlem  16548  3lcm2e6woprm  16639  6lcm4e12  16640  modxai  17093  mod2xnegi  17096  karatsuba  17108  sinhalfpilem  26429  ef2pi  26443  ef2kpi  26444  efper  26445  sinperlem  26446  sin2kpi  26449  cos2kpi  26450  sin2pim  26451  cos2pim  26452  sincos4thpi  26479  sincos6thpi  26482  pige3ALT  26486  abssinper  26487  efeq1  26494  logi  26553  logneg  26554  logm1  26555  eflogeq  26568  logimul  26580  logneg2  26581  cxpsqrt  26669  root1eq1  26722  cxpeq  26724  ang180lem1  26776  ang180lem3  26778  ang180lem4  26779  1cubrlem  26808  1cubr  26809  quart1lem  26822  asin1  26861  atanlogsublem  26882  log2ublem2  26914  log2ublem3  26915  log2ub  26916  bclbnd  27248  bposlem8  27259  bposlem9  27260  lgsdir2lem5  27297  2lgsoddprmlem3c  27380  2lgsoddprmlem3d  27381  ax5seglem7  28919  ip0i  30811  ip1ilem  30812  ipasslem10  30825  siilem1  30837  normlem0  31095  normlem1  31096  normlem2  31097  normlem3  31098  normlem5  31100  normlem7  31102  bcseqi  31106  norm-ii-i  31123  normpar2i  31142  polid2i  31143  h1de2i  31539  lnopunilem1  31996  lnophmlem2  32003  dfdec100  32814  dpmul100  32876  dp3mul10  32877  dpmul1000  32878  dpexpp1  32887  dpmul  32892  dpmul4  32893  cos9thpiminplylem4  33824  cos9thpiminplylem5  33825  ballotth  34575  efmul2picn  34633  itgexpif  34643  vtscl  34675  circlemeth  34677  hgt750lem  34688  problem2  35693  problem4  35695  quad3  35697  heiborlem6  37845  gcdaddmzz2nncomi  42013  sn-1ne2  42283  sqsumi  42299  sqmid3api  42301  sqdeccom12  42307  cxp112d  42359  cxp111d  42360  cxpi11d  42361  re1m1e0m0  42415  reixi  42440  sn-1ticom  42452  sn-0tie0  42457  sn-inelr  42485  proot1ex  43195  areaquad  43215  resqrtvalex  43644  imsqrtvalex  43645  coskpi2  45875  cosnegpi  45876  cosknegpi  45878  wallispilem4  46077  dirkerper  46105  dirkertrigeq  46110  dirkercncflem2  46113  fourierdlem57  46172  fourierdlem62  46177  fourierswlem  46239  fmtnorec3  47542  fmtnorec4  47543  lighneallem3  47601  3exp4mod41  47610  41prothprmlem1  47611  zlmodzxzequap  48455  nn0sumshdiglemB  48580  i2linesi  49622