Theorem mulcli 11326

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

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℂcc 11208   · cmul 11215

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 11272

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mul02lem2  11497  addrid  11500  cnegex2  11502  ixi  11955  2mulicn  12580  numma  12873  nummac  12874  9t11e99OLD  12960  decbin2  12972  irec  14355  binom2i  14366  crreczi  14382  3dec  14420  nn0opthi  14424  faclbnd4lem1  14447  rei  15335  imi  15336  iseraltlem2  15862  bpoly3  16236  bpoly4  16237  3dvdsdec  16514  3dvds2dec  16515  odd2np1  16523  gcdaddmlem  16708  3lcm2e6woprm  16802  6lcm4e12  16803  modxai  17258  mod2xnegi  17261  karatsuba  17273  2picn  26798  sinhalfpilem  26804  ef2pi  26818  ef2kpi  26819  efper  26820  sinperlem  26821  sin2kpi  26824  cos2kpi  26825  sin2pim  26826  cos2pim  26827  sincos4thpi  26854  sincos6thpi  26856  pige3ALT  26860  abssinper  26861  logi  26927  logneg  26928  logm1  26929  eflogeq  26942  logimul  26954  logneg2  26955  cxpsqrt  27043  root1eq1  27095  cxpeq  27097  ang180lem1  27149  ang180lem4  27152  1cubrlem  27181  1cubr  27182  quart1lem  27195  asin1  27234  atanlogsublem  27255  log2ublem2  27287  log2ublem3  27288  log2ub  27289  bclbnd  27619  bposlem8  27630  bposlem9  27631  lgsdir2lem5  27668  2lgsoddprmlem3c  27751  2lgsoddprmlem3d  27752  ax5seglem7  29525  ip0i  31439  ip1ilem  31440  ipasslem10  31453  siilem1  31465  normlem0  31723  normlem1  31724  normlem2  31725  normlem3  31726  normlem5  31728  normlem7  31730  bcseqi  31734  norm-ii-i  31751  normpar2i  31770  polid2i  31771  h1de2i  32167  lnopunilem1  32624  lnophmlem2  32631  dfdec100  33474  dpmul100  33516  dp3mul10  33517  dpmul1000  33518  dpexpp1  33527  dpmul  33532  dpmul4  33533  cos9thpiminplylem4  34470  cos9thpiminplylem5  34471  ballotth  35223  efmul2picn  35278  itgexpif  35288  vtscl  35320  circlemeth  35322  hgt750lem  35333  problem2  36552  problem4  36554  quad3  36556  heiborlem6  38890  gcdaddmzz2nncomi  43185  25or6to4  43396  sn-1ne2  43470  sqsumi  43478  sqmid3api  43480  sqdeccom12  43486  cxp112d  43532  cxp111d  43533  cxpi11d  43534  re1m1e0m0  43588  reixi  43614  sn-1ticom  43626  sn-0tie0  43655  proot1ex  44338  areaquad  44358  resqrtvalex  44785  imsqrtvalex  44786  coskpi2  47015  cosnegpi  47016  cosknegpi  47018  wallispilem4  47217  dirkertrigeq  47250  fourierdlem57  47312  fourierdlem62  47317  fourierswlem  47379  cos5t  48064  goldpolyfactor  48066  goldrasin  48068  goldratmolem3  48073  goldratmolem4  48074  fmtnorec3  48772  fmtnorec4  48773  lighneallem3  48831  3exp4mod41  48840  41prothprmlem1  48841  zlmodzxzequap  49750  nn0sumshdiglemB  49871  i2linesi  51088