Theorem mulcli 11181

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   · cmul 11073

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

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

This theorem is referenced by:  mul02lem2  11351  addrid  11354  cnegex2  11356  ixi  11807  2mulicn  12406  numma  12693  nummac  12694  9t11e99  12779  decbin2  12790  irec  14166  binom2i  14177  crreczi  14193  3dec  14231  nn0opthi  14235  faclbnd4lem1  14258  rei  15122  imi  15123  iseraltlem2  15649  bpoly3  16024  bpoly4  16025  3dvdsdec  16302  3dvds2dec  16303  odd2np1  16311  gcdaddmlem  16494  3lcm2e6woprm  16585  6lcm4e12  16586  modxai  17039  mod2xnegi  17042  karatsuba  17054  sinhalfpilem  26372  ef2pi  26386  ef2kpi  26387  efper  26388  sinperlem  26389  sin2kpi  26392  cos2kpi  26393  sin2pim  26394  cos2pim  26395  sincos4thpi  26422  sincos6thpi  26425  pige3ALT  26429  abssinper  26430  efeq1  26437  logi  26496  logneg  26497  logm1  26498  eflogeq  26511  logimul  26523  logneg2  26524  cxpsqrt  26612  root1eq1  26665  cxpeq  26667  ang180lem1  26719  ang180lem3  26721  ang180lem4  26722  1cubrlem  26751  1cubr  26752  quart1lem  26765  asin1  26804  atanlogsublem  26825  log2ublem2  26857  log2ublem3  26858  log2ub  26859  bclbnd  27191  bposlem8  27202  bposlem9  27203  lgsdir2lem5  27240  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  ax5seglem7  28862  ip0i  30754  ip1ilem  30755  ipasslem10  30768  siilem1  30780  normlem0  31038  normlem1  31039  normlem2  31040  normlem3  31041  normlem5  31043  normlem7  31045  bcseqi  31049  norm-ii-i  31066  normpar2i  31085  polid2i  31086  h1de2i  31482  lnopunilem1  31939  lnophmlem2  31946  dfdec100  32755  dpmul100  32817  dp3mul10  32818  dpmul1000  32819  dpexpp1  32828  dpmul  32833  dpmul4  32834  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  ballotth  34529  efmul2picn  34587  itgexpif  34597  vtscl  34629  circlemeth  34631  hgt750lem  34642  problem2  35653  problem4  35655  quad3  35657  heiborlem6  37810  gcdaddmzz2nncomi  41983  sn-1ne2  42253  sqsumi  42269  sqmid3api  42271  sqdeccom12  42277  cxp112d  42329  cxp111d  42330  cxpi11d  42331  re1m1e0m0  42385  reixi  42411  sn-1ticom  42423  sn-0tie0  42439  proot1ex  43185  areaquad  43205  resqrtvalex  43634  imsqrtvalex  43635  coskpi2  45864  cosnegpi  45865  cosknegpi  45867  wallispilem4  46066  dirkerper  46094  dirkertrigeq  46099  dirkercncflem2  46102  fourierdlem57  46161  fourierdlem62  46166  fourierswlem  46228  fmtnorec3  47549  fmtnorec4  47550  lighneallem3  47608  3exp4mod41  47617  41prothprmlem1  47618  zlmodzxzequap  48488  nn0sumshdiglemB  48609  i2linesi  49767