Theorem mulcli 11243

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

Syntax hints:   ∈ wcel 2099  (class class class)co 7414  ℂcc 11128   · cmul 11135

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

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

This theorem is referenced by:  mul02lem2  11413  addrid  11416  cnegex2  11418  ixi  11865  2mulicn  12457  numma  12743  nummac  12744  9t11e99  12829  decbin2  12840  irec  14188  binom2i  14199  crreczi  14214  3dec  14249  nn0opthi  14253  faclbnd4lem1  14276  rei  15127  imi  15128  iseraltlem2  15653  bpoly3  16026  bpoly4  16027  3dvdsdec  16300  3dvds2dec  16301  odd2np1  16309  gcdaddmlem  16490  3lcm2e6woprm  16577  6lcm4e12  16578  modxai  17028  mod2xnegi  17031  decexp2  17035  karatsuba  17044  sinhalfpilem  26385  ef2pi  26399  ef2kpi  26400  efper  26401  sinperlem  26402  sin2kpi  26405  cos2kpi  26406  sin2pim  26407  cos2pim  26408  sincos4thpi  26435  sincos6thpi  26437  pige3ALT  26441  abssinper  26442  efeq1  26449  logi  26508  logneg  26509  logm1  26510  eflogeq  26523  logimul  26535  logneg2  26536  cxpsqrt  26624  root1eq1  26677  cxpeq  26679  ang180lem1  26728  ang180lem3  26730  ang180lem4  26731  1cubrlem  26760  1cubr  26761  quart1lem  26774  asin1  26813  atanlogsublem  26834  log2ublem2  26866  log2ublem3  26867  log2ub  26868  bclbnd  27200  bposlem8  27211  bposlem9  27212  lgsdir2lem5  27249  2lgsoddprmlem3c  27332  2lgsoddprmlem3d  27333  ax5seglem7  28733  ip0i  30622  ip1ilem  30623  ipasslem10  30636  siilem1  30648  normlem0  30906  normlem1  30907  normlem2  30908  normlem3  30909  normlem5  30911  normlem7  30913  bcseqi  30917  norm-ii-i  30934  normpar2i  30953  polid2i  30954  h1de2i  31350  lnopunilem1  31807  lnophmlem2  31814  dfdec100  32575  dpmul100  32602  dp3mul10  32603  dpmul1000  32604  dpexpp1  32613  dpmul  32618  dpmul4  32619  ballotth  34093  efmul2picn  34164  itgexpif  34174  vtscl  34206  circlemeth  34208  hgt750lem  34219  problem2  35206  problem4  35208  quad3  35210  heiborlem6  37224  gcdaddmzz2nncomi  41403  sn-1ne2  41762  sqsumi  41777  sqmid3api  41779  sqdeccom12  41785  cxp112d  41834  cxp111d  41835  cxpi11d  41836  re1m1e0m0  41874  reixi  41899  sn-1ticom  41911  sn-0tie0  41916  sn-inelr  41942  proot1ex  42546  areaquad  42567  resqrtvalex  42998  imsqrtvalex  42999  coskpi2  45177  cosnegpi  45178  cosknegpi  45180  wallispilem4  45379  dirkerper  45407  dirkertrigeq  45412  dirkercncflem2  45415  fourierdlem57  45474  fourierdlem62  45479  fourierswlem  45541  fmtnorec3  46811  fmtnorec4  46812  lighneallem3  46870  3exp4mod41  46879  41prothprmlem1  46880  zlmodzxzequap  47490  nn0sumshdiglemB  47616  i2linesi  48134