Theorem mulcli 11204

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

Syntax hints:   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086   · cmul 11093

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  mul02lem2  11375  addrid  11378  cnegex2  11380  ixi  11831  2mulicn  12456  numma  12748  nummac  12749  9t11e99OLD  12835  decbin2  12847  irec  14225  binom2i  14236  crreczi  14252  3dec  14290  nn0opthi  14294  faclbnd4lem1  14317  rei  15195  imi  15196  iseraltlem2  15722  bpoly3  16100  bpoly4  16101  3dvdsdec  16378  3dvds2dec  16379  odd2np1  16387  gcdaddmlem  16570  3lcm2e6woprm  16661  6lcm4e12  16662  modxai  17116  mod2xnegi  17119  karatsuba  17131  2picn  26576  sinhalfpilem  26582  ef2pi  26596  ef2kpi  26597  efper  26598  sinperlem  26599  sin2kpi  26602  cos2kpi  26603  sin2pim  26604  cos2pim  26605  sincos4thpi  26632  sincos6thpi  26635  pige3ALT  26639  abssinper  26640  efeq1  26647  logi  26706  logneg  26707  logm1  26708  eflogeq  26721  logimul  26733  logneg2  26734  cxpsqrt  26822  root1eq1  26874  cxpeq  26876  ang180lem1  26928  ang180lem3  26930  ang180lem4  26931  1cubrlem  26960  1cubr  26961  quart1lem  26974  asin1  27013  atanlogsublem  27034  log2ublem2  27066  log2ublem3  27067  log2ub  27068  bclbnd  27398  bposlem8  27409  bposlem9  27410  lgsdir2lem5  27447  2lgsoddprmlem3c  27530  2lgsoddprmlem3d  27531  ax5seglem7  29190  ip0i  31082  ip1ilem  31083  ipasslem10  31096  siilem1  31108  normlem0  31366  normlem1  31367  normlem2  31368  normlem3  31369  normlem5  31371  normlem7  31373  bcseqi  31377  norm-ii-i  31394  normpar2i  31413  polid2i  31414  h1de2i  31810  lnopunilem1  32267  lnophmlem2  32274  dfdec100  33082  dpmul100  33124  dp3mul10  33125  dpmul1000  33126  dpexpp1  33135  dpmul  33140  dpmul4  33141  cos9thpiminplylem4  34087  cos9thpiminplylem5  34088  ballotth  34840  efmul2picn  34895  itgexpif  34905  vtscl  34937  circlemeth  34939  hgt750lem  34950  problem2  36024  problem4  36026  quad3  36028  heiborlem6  38322  gcdaddmzz2nncomi  42619  sn-1ne2  42887  sqsumi  42897  sqmid3api  42899  sqdeccom12  42905  cxp112d  42957  cxp111d  42958  cxpi11d  42959  re1m1e0m0  43013  reixi  43039  sn-1ticom  43051  sn-0tie0  43080  proot1ex  43780  areaquad  43800  resqrtvalex  44228  imsqrtvalex  44229  coskpi2  46439  cosnegpi  46440  cosknegpi  46442  wallispilem4  46641  dirkertrigeq  46674  fourierdlem57  46736  fourierdlem62  46741  fourierswlem  46803  cos5t  47472  goldrasin  47475  fmtnorec3  48156  fmtnorec4  48157  lighneallem3  48215  3exp4mod41  48224  41prothprmlem1  48225  zlmodzxzequap  49131  nn0sumshdiglemB  49252  i2linesi  50408