Theorem mulcli 10840

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

Syntax hints:   ∈ wcel 2110  (class class class)co 7213  ℂcc 10727   · cmul 10734

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

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

This theorem is referenced by:  mul02lem2  11009  addid1  11012  cnegex2  11014  ixi  11461  2mulicn  12053  numma  12337  nummac  12338  9t11e99  12423  decbin2  12434  irec  13770  binom2i  13780  crreczi  13795  3dec  13832  nn0opthi  13836  faclbnd4lem1  13859  rei  14719  imi  14720  iseraltlem2  15246  bpoly3  15620  bpoly4  15621  3dvdsdec  15893  3dvds2dec  15894  odd2np1  15902  gcdaddmlem  16083  3lcm2e6woprm  16172  6lcm4e12  16173  modxai  16621  mod2xnegi  16624  decexp2  16628  karatsuba  16637  sinhalfpilem  25353  ef2pi  25367  ef2kpi  25368  efper  25369  sinperlem  25370  sin2kpi  25373  cos2kpi  25374  sin2pim  25375  cos2pim  25376  sincos4thpi  25403  sincos6thpi  25405  pige3ALT  25409  abssinper  25410  efeq1  25417  logneg  25476  logm1  25477  eflogeq  25490  logimul  25502  logneg2  25503  cxpsqrt  25591  root1eq1  25641  cxpeq  25643  ang180lem1  25692  ang180lem3  25694  ang180lem4  25695  1cubrlem  25724  1cubr  25725  quart1lem  25738  asin1  25777  atanlogsublem  25798  log2ublem2  25830  log2ublem3  25831  log2ub  25832  bclbnd  26161  bposlem8  26172  bposlem9  26173  lgsdir2lem5  26210  2lgsoddprmlem3c  26293  2lgsoddprmlem3d  26294  ax5seglem7  27026  ip0i  28906  ip1ilem  28907  ipasslem10  28920  siilem1  28932  normlem0  29190  normlem1  29191  normlem2  29192  normlem3  29193  normlem5  29195  normlem7  29197  bcseqi  29201  norm-ii-i  29218  normpar2i  29237  polid2i  29238  h1de2i  29634  lnopunilem1  30091  lnophmlem2  30098  dfdec100  30864  dpmul100  30891  dp3mul10  30892  dpmul1000  30893  dpexpp1  30902  dpmul  30907  dpmul4  30908  ballotth  32216  efmul2picn  32288  itgexpif  32298  vtscl  32330  circlemeth  32332  hgt750lem  32343  problem2  33337  problem4  33339  quad3  33341  logi  33418  heiborlem6  35711  gcdaddmzz2nncomi  39738  sn-1ne2  40002  sqsumi  40016  sqmid3api  40018  sqdeccom12  40024  re1m1e0m0  40088  reixi  40112  sn-1ticom  40124  sn-0tie0  40129  sn-inelr  40143  proot1ex  40729  areaquad  40750  resqrtvalex  40929  imsqrtvalex  40930  coskpi2  43082  cosnegpi  43083  cosknegpi  43085  wallispilem4  43284  dirkerper  43312  dirkertrigeq  43317  dirkercncflem2  43320  fourierdlem57  43379  fourierdlem62  43384  fourierswlem  43446  fmtnorec3  44673  fmtnorec4  44674  lighneallem3  44732  3exp4mod41  44741  41prothprmlem1  44742  zlmodzxzequap  45513  nn0sumshdiglemB  45639  i2linesi  46153