Theorem mulcli 11225

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

Syntax hints:   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110   · cmul 11117

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

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

This theorem is referenced by:  mul02lem2  11395  addrid  11398  cnegex2  11400  ixi  11847  2mulicn  12439  numma  12725  nummac  12726  9t11e99  12811  decbin2  12822  irec  14169  binom2i  14180  crreczi  14195  3dec  14230  nn0opthi  14234  faclbnd4lem1  14257  rei  15107  imi  15108  iseraltlem2  15633  bpoly3  16006  bpoly4  16007  3dvdsdec  16279  3dvds2dec  16280  odd2np1  16288  gcdaddmlem  16469  3lcm2e6woprm  16556  6lcm4e12  16557  modxai  17005  mod2xnegi  17008  decexp2  17012  karatsuba  17021  sinhalfpilem  26209  ef2pi  26223  ef2kpi  26224  efper  26225  sinperlem  26226  sin2kpi  26229  cos2kpi  26230  sin2pim  26231  cos2pim  26232  sincos4thpi  26259  sincos6thpi  26261  pige3ALT  26265  abssinper  26266  efeq1  26273  logneg  26332  logm1  26333  eflogeq  26346  logimul  26358  logneg2  26359  cxpsqrt  26447  root1eq1  26499  cxpeq  26501  ang180lem1  26550  ang180lem3  26552  ang180lem4  26553  1cubrlem  26582  1cubr  26583  quart1lem  26596  asin1  26635  atanlogsublem  26656  log2ublem2  26688  log2ublem3  26689  log2ub  26690  bclbnd  27019  bposlem8  27030  bposlem9  27031  lgsdir2lem5  27068  2lgsoddprmlem3c  27151  2lgsoddprmlem3d  27152  ax5seglem7  28460  ip0i  30345  ip1ilem  30346  ipasslem10  30359  siilem1  30371  normlem0  30629  normlem1  30630  normlem2  30631  normlem3  30632  normlem5  30634  normlem7  30636  bcseqi  30640  norm-ii-i  30657  normpar2i  30676  polid2i  30677  h1de2i  31073  lnopunilem1  31530  lnophmlem2  31537  dfdec100  32303  dpmul100  32330  dp3mul10  32331  dpmul1000  32332  dpexpp1  32341  dpmul  32346  dpmul4  32347  ballotth  33834  efmul2picn  33906  itgexpif  33916  vtscl  33948  circlemeth  33950  hgt750lem  33961  problem2  34949  problem4  34951  quad3  34953  logi  35008  heiborlem6  36987  gcdaddmzz2nncomi  41167  sn-1ne2  41481  sqsumi  41495  sqmid3api  41497  sqdeccom12  41503  re1m1e0m0  41572  reixi  41597  sn-1ticom  41609  sn-0tie0  41614  sn-inelr  41640  proot1ex  42245  areaquad  42267  resqrtvalex  42698  imsqrtvalex  42699  coskpi2  44880  cosnegpi  44881  cosknegpi  44883  wallispilem4  45082  dirkerper  45110  dirkertrigeq  45115  dirkercncflem2  45118  fourierdlem57  45177  fourierdlem62  45182  fourierswlem  45244  fmtnorec3  46514  fmtnorec4  46515  lighneallem3  46573  3exp4mod41  46582  41prothprmlem1  46583  zlmodzxzequap  47267  nn0sumshdiglemB  47393  i2linesi  47912