Theorem mulcli 11251

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

Syntax hints:   ∈ wcel 2098  (class class class)co 7417  ℂcc 11136   · cmul 11143

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

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

This theorem is referenced by:  mul02lem2  11421  addrid  11424  cnegex2  11426  ixi  11873  2mulicn  12465  numma  12751  nummac  12752  9t11e99  12837  decbin2  12848  irec  14196  binom2i  14207  crreczi  14222  3dec  14257  nn0opthi  14261  faclbnd4lem1  14284  rei  15135  imi  15136  iseraltlem2  15661  bpoly3  16034  bpoly4  16035  3dvdsdec  16308  3dvds2dec  16309  odd2np1  16317  gcdaddmlem  16498  3lcm2e6woprm  16585  6lcm4e12  16586  modxai  17036  mod2xnegi  17039  decexp2  17043  karatsuba  17052  sinhalfpilem  26428  ef2pi  26442  ef2kpi  26443  efper  26444  sinperlem  26445  sin2kpi  26448  cos2kpi  26449  sin2pim  26450  cos2pim  26451  sincos4thpi  26478  sincos6thpi  26480  pige3ALT  26484  abssinper  26485  efeq1  26492  logi  26551  logneg  26552  logm1  26553  eflogeq  26566  logimul  26578  logneg2  26579  cxpsqrt  26667  root1eq1  26720  cxpeq  26722  ang180lem1  26771  ang180lem3  26773  ang180lem4  26774  1cubrlem  26803  1cubr  26804  quart1lem  26817  asin1  26856  atanlogsublem  26877  log2ublem2  26909  log2ublem3  26910  log2ub  26911  bclbnd  27243  bposlem8  27254  bposlem9  27255  lgsdir2lem5  27292  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  ax5seglem7  28802  ip0i  30691  ip1ilem  30692  ipasslem10  30705  siilem1  30717  normlem0  30975  normlem1  30976  normlem2  30977  normlem3  30978  normlem5  30980  normlem7  30982  bcseqi  30986  norm-ii-i  31003  normpar2i  31022  polid2i  31023  h1de2i  31419  lnopunilem1  31876  lnophmlem2  31883  dfdec100  32650  dpmul100  32677  dp3mul10  32678  dpmul1000  32679  dpexpp1  32688  dpmul  32693  dpmul4  32694  ballotth  34227  efmul2picn  34298  itgexpif  34308  vtscl  34340  circlemeth  34342  hgt750lem  34353  problem2  35340  problem4  35342  quad3  35344  heiborlem6  37359  gcdaddmzz2nncomi  41535  sn-1ne2  41905  sqsumi  41920  sqmid3api  41922  sqdeccom12  41928  cxp112d  41977  cxp111d  41978  cxpi11d  41979  re1m1e0m0  42017  reixi  42042  sn-1ticom  42054  sn-0tie0  42059  sn-inelr  42085  proot1ex  42689  areaquad  42709  resqrtvalex  43140  imsqrtvalex  43141  coskpi2  45317  cosnegpi  45318  cosknegpi  45320  wallispilem4  45519  dirkerper  45547  dirkertrigeq  45552  dirkercncflem2  45555  fourierdlem57  45614  fourierdlem62  45619  fourierswlem  45681  fmtnorec3  46951  fmtnorec4  46952  lighneallem3  47010  3exp4mod41  47019  41prothprmlem1  47020  zlmodzxzequap  47679  nn0sumshdiglemB  47805  i2linesi  48323