Theorem mulcli 11190

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

Syntax hints:   ∈ wcel 2143  (class class class)co 7397  ℂcc 11072   · cmul 11079

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

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  mul02lem2  11361  addrid  11364  cnegex2  11366  ixi  11817  2mulicn  12446  numma  12738  nummac  12739  9t11e99OLD  12825  decbin2  12837  irec  14215  binom2i  14226  crreczi  14242  3dec  14280  nn0opthi  14284  faclbnd4lem1  14307  rei  15184  imi  15185  iseraltlem2  15711  bpoly3  16089  bpoly4  16090  3dvdsdec  16367  3dvds2dec  16368  odd2np1  16376  gcdaddmlem  16559  3lcm2e6woprm  16650  6lcm4e12  16651  modxai  17105  mod2xnegi  17108  karatsuba  17120  2picn  26523  sinhalfpilem  26529  ef2pi  26543  ef2kpi  26544  efper  26545  sinperlem  26546  sin2kpi  26549  cos2kpi  26550  sin2pim  26551  cos2pim  26552  sincos4thpi  26579  sincos6thpi  26582  pige3ALT  26586  abssinper  26587  efeq1  26594  logi  26653  logneg  26654  logm1  26655  eflogeq  26668  logimul  26680  logneg2  26681  cxpsqrt  26769  root1eq1  26821  cxpeq  26823  ang180lem1  26875  ang180lem3  26877  ang180lem4  26878  1cubrlem  26907  1cubr  26908  quart1lem  26921  asin1  26960  atanlogsublem  26981  log2ublem2  27013  log2ublem3  27014  log2ub  27015  bclbnd  27345  bposlem8  27356  bposlem9  27357  lgsdir2lem5  27394  2lgsoddprmlem3c  27477  2lgsoddprmlem3d  27478  ax5seglem7  29137  ip0i  31029  ip1ilem  31030  ipasslem10  31043  siilem1  31055  normlem0  31313  normlem1  31314  normlem2  31315  normlem3  31316  normlem5  31318  normlem7  31320  bcseqi  31324  norm-ii-i  31341  normpar2i  31360  polid2i  31361  h1de2i  31757  lnopunilem1  32214  lnophmlem2  32221  dfdec100  33033  dpmul100  33075  dp3mul10  33076  dpmul1000  33077  dpexpp1  33086  dpmul  33091  dpmul4  33092  cos9thpiminplylem4  34083  cos9thpiminplylem5  34084  ballotth  34836  efmul2picn  34891  itgexpif  34901  vtscl  34933  circlemeth  34935  hgt750lem  34946  problem2  36017  problem4  36019  quad3  36021  heiborlem6  38316  gcdaddmzz2nncomi  42613  sn-1ne2  42881  sqsumi  42891  sqmid3api  42893  sqdeccom12  42899  cxp112d  42951  cxp111d  42952  cxpi11d  42953  re1m1e0m0  43007  reixi  43033  sn-1ticom  43045  sn-0tie0  43074  proot1ex  43774  areaquad  43794  resqrtvalex  44222  imsqrtvalex  44223  coskpi2  46441  cosnegpi  46442  cosknegpi  46444  wallispilem4  46643  dirkertrigeq  46676  fourierdlem57  46738  fourierdlem62  46743  fourierswlem  46805  cos5t  47474  goldrasin  47477  fmtnorec3  48158  fmtnorec4  48159  lighneallem3  48217  3exp4mod41  48226  41prothprmlem1  48227  zlmodzxzequap  49122  nn0sumshdiglemB  49243  i2linesi  50400