Theorem mulcli 11171

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

Syntax hints:   ∈ wcel 2106  (class class class)co 7362  ℂcc 11058   · cmul 11065

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

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

This theorem is referenced by:  mul02lem2  11341  addrid  11344  cnegex2  11346  ixi  11793  2mulicn  12385  numma  12671  nummac  12672  9t11e99  12757  decbin2  12768  irec  14115  binom2i  14126  crreczi  14141  3dec  14176  nn0opthi  14180  faclbnd4lem1  14203  rei  15053  imi  15054  iseraltlem2  15579  bpoly3  15952  bpoly4  15953  3dvdsdec  16225  3dvds2dec  16226  odd2np1  16234  gcdaddmlem  16415  3lcm2e6woprm  16502  6lcm4e12  16503  modxai  16951  mod2xnegi  16954  decexp2  16958  karatsuba  16967  sinhalfpilem  25857  ef2pi  25871  ef2kpi  25872  efper  25873  sinperlem  25874  sin2kpi  25877  cos2kpi  25878  sin2pim  25879  cos2pim  25880  sincos4thpi  25907  sincos6thpi  25909  pige3ALT  25913  abssinper  25914  efeq1  25921  logneg  25980  logm1  25981  eflogeq  25994  logimul  26006  logneg2  26007  cxpsqrt  26095  root1eq1  26145  cxpeq  26147  ang180lem1  26196  ang180lem3  26198  ang180lem4  26199  1cubrlem  26228  1cubr  26229  quart1lem  26242  asin1  26281  atanlogsublem  26302  log2ublem2  26334  log2ublem3  26335  log2ub  26336  bclbnd  26665  bposlem8  26676  bposlem9  26677  lgsdir2lem5  26714  2lgsoddprmlem3c  26797  2lgsoddprmlem3d  26798  ax5seglem7  27947  ip0i  29830  ip1ilem  29831  ipasslem10  29844  siilem1  29856  normlem0  30114  normlem1  30115  normlem2  30116  normlem3  30117  normlem5  30119  normlem7  30121  bcseqi  30125  norm-ii-i  30142  normpar2i  30161  polid2i  30162  h1de2i  30558  lnopunilem1  31015  lnophmlem2  31022  dfdec100  31796  dpmul100  31823  dp3mul10  31824  dpmul1000  31825  dpexpp1  31834  dpmul  31839  dpmul4  31840  ballotth  33226  efmul2picn  33298  itgexpif  33308  vtscl  33340  circlemeth  33342  hgt750lem  33353  problem2  34341  problem4  34343  quad3  34345  logi  34393  heiborlem6  36348  gcdaddmzz2nncomi  40526  sn-1ne2  40839  sqsumi  40853  sqmid3api  40855  sqdeccom12  40861  re1m1e0m0  40924  reixi  40949  sn-1ticom  40961  sn-0tie0  40966  sn-inelr  40992  proot1ex  41586  areaquad  41608  resqrtvalex  42039  imsqrtvalex  42040  coskpi2  44227  cosnegpi  44228  cosknegpi  44230  wallispilem4  44429  dirkerper  44457  dirkertrigeq  44462  dirkercncflem2  44465  fourierdlem57  44524  fourierdlem62  44529  fourierswlem  44591  fmtnorec3  45860  fmtnorec4  45861  lighneallem3  45919  3exp4mod41  45928  41prothprmlem1  45929  zlmodzxzequap  46700  nn0sumshdiglemB  46826  i2linesi  47345