Theorem mulcli 11137

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

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022   · cmul 11029

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

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

This theorem is referenced by:  mul02lem2  11308  addrid  11311  cnegex2  11313  ixi  11764  2mulicn  12363  numma  12649  nummac  12650  9t11e99  12735  decbin2  12746  irec  14122  binom2i  14133  crreczi  14149  3dec  14187  nn0opthi  14191  faclbnd4lem1  14214  rei  15077  imi  15078  iseraltlem2  15604  bpoly3  15979  bpoly4  15980  3dvdsdec  16257  3dvds2dec  16258  odd2np1  16266  gcdaddmlem  16449  3lcm2e6woprm  16540  6lcm4e12  16541  modxai  16994  mod2xnegi  16997  karatsuba  17009  sinhalfpilem  26426  ef2pi  26440  ef2kpi  26441  efper  26442  sinperlem  26443  sin2kpi  26446  cos2kpi  26447  sin2pim  26448  cos2pim  26449  sincos4thpi  26476  sincos6thpi  26479  pige3ALT  26483  abssinper  26484  efeq1  26491  logi  26550  logneg  26551  logm1  26552  eflogeq  26565  logimul  26577  logneg2  26578  cxpsqrt  26666  root1eq1  26719  cxpeq  26721  ang180lem1  26773  ang180lem3  26775  ang180lem4  26776  1cubrlem  26805  1cubr  26806  quart1lem  26819  asin1  26858  atanlogsublem  26879  log2ublem2  26911  log2ublem3  26912  log2ub  26913  bclbnd  27245  bposlem8  27256  bposlem9  27257  lgsdir2lem5  27294  2lgsoddprmlem3c  27377  2lgsoddprmlem3d  27378  ax5seglem7  28957  ip0i  30849  ip1ilem  30850  ipasslem10  30863  siilem1  30875  normlem0  31133  normlem1  31134  normlem2  31135  normlem3  31136  normlem5  31138  normlem7  31140  bcseqi  31144  norm-ii-i  31161  normpar2i  31180  polid2i  31181  h1de2i  31577  lnopunilem1  32034  lnophmlem2  32041  dfdec100  32860  dpmul100  32927  dp3mul10  32928  dpmul1000  32929  dpexpp1  32938  dpmul  32943  dpmul4  32944  cos9thpiminplylem4  33891  cos9thpiminplylem5  33892  ballotth  34644  efmul2picn  34702  itgexpif  34712  vtscl  34744  circlemeth  34746  hgt750lem  34757  problem2  35809  problem4  35811  quad3  35813  heiborlem6  37956  gcdaddmzz2nncomi  42188  sn-1ne2  42462  sqsumi  42478  sqmid3api  42480  sqdeccom12  42486  cxp112d  42538  cxp111d  42539  cxpi11d  42540  re1m1e0m0  42594  reixi  42620  sn-1ticom  42632  sn-0tie0  42648  proot1ex  43380  areaquad  43400  resqrtvalex  43828  imsqrtvalex  43829  coskpi2  46052  cosnegpi  46053  cosknegpi  46055  wallispilem4  46254  dirkerper  46282  dirkertrigeq  46287  dirkercncflem2  46290  fourierdlem57  46349  fourierdlem62  46354  fourierswlem  46416  fmtnorec3  47736  fmtnorec4  47737  lighneallem3  47795  3exp4mod41  47804  41prothprmlem1  47805  zlmodzxzequap  48687  nn0sumshdiglemB  48808  i2linesi  49965