Theorem mulcli 11221

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

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   · cmul 11115

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

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  mul02lem2  11391  addrid  11394  cnegex2  11396  ixi  11843  2mulicn  12435  numma  12721  nummac  12722  9t11e99  12807  decbin2  12818  irec  14165  binom2i  14176  crreczi  14191  3dec  14226  nn0opthi  14230  faclbnd4lem1  14253  rei  15103  imi  15104  iseraltlem2  15629  bpoly3  16002  bpoly4  16003  3dvdsdec  16275  3dvds2dec  16276  odd2np1  16284  gcdaddmlem  16465  3lcm2e6woprm  16552  6lcm4e12  16553  modxai  17001  mod2xnegi  17004  decexp2  17008  karatsuba  17017  sinhalfpilem  25973  ef2pi  25987  ef2kpi  25988  efper  25989  sinperlem  25990  sin2kpi  25993  cos2kpi  25994  sin2pim  25995  cos2pim  25996  sincos4thpi  26023  sincos6thpi  26025  pige3ALT  26029  abssinper  26030  efeq1  26037  logneg  26096  logm1  26097  eflogeq  26110  logimul  26122  logneg2  26123  cxpsqrt  26211  root1eq1  26263  cxpeq  26265  ang180lem1  26314  ang180lem3  26316  ang180lem4  26317  1cubrlem  26346  1cubr  26347  quart1lem  26360  asin1  26399  atanlogsublem  26420  log2ublem2  26452  log2ublem3  26453  log2ub  26454  bclbnd  26783  bposlem8  26794  bposlem9  26795  lgsdir2lem5  26832  2lgsoddprmlem3c  26915  2lgsoddprmlem3d  26916  ax5seglem7  28193  ip0i  30078  ip1ilem  30079  ipasslem10  30092  siilem1  30104  normlem0  30362  normlem1  30363  normlem2  30364  normlem3  30365  normlem5  30367  normlem7  30369  bcseqi  30373  norm-ii-i  30390  normpar2i  30409  polid2i  30410  h1de2i  30806  lnopunilem1  31263  lnophmlem2  31270  dfdec100  32036  dpmul100  32063  dp3mul10  32064  dpmul1000  32065  dpexpp1  32074  dpmul  32079  dpmul4  32080  ballotth  33536  efmul2picn  33608  itgexpif  33618  vtscl  33650  circlemeth  33652  hgt750lem  33663  problem2  34651  problem4  34653  quad3  34655  logi  34704  heiborlem6  36684  gcdaddmzz2nncomi  40861  sn-1ne2  41179  sqsumi  41193  sqmid3api  41195  sqdeccom12  41201  re1m1e0m0  41270  reixi  41295  sn-1ticom  41307  sn-0tie0  41312  sn-inelr  41338  proot1ex  41943  areaquad  41965  resqrtvalex  42396  imsqrtvalex  42397  coskpi2  44582  cosnegpi  44583  cosknegpi  44585  wallispilem4  44784  dirkerper  44812  dirkertrigeq  44817  dirkercncflem2  44820  fourierdlem57  44879  fourierdlem62  44884  fourierswlem  44946  fmtnorec3  46216  fmtnorec4  46217  lighneallem3  46275  3exp4mod41  46284  41prothprmlem1  46285  zlmodzxzequap  47180  nn0sumshdiglemB  47306  i2linesi  47825