Theorem mulcli 11216

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

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℂcc 11098   · cmul 11105

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  mul02lem2  11387  addrid  11390  cnegex2  11392  ixi  11843  2mulicn  12468  numma  12760  nummac  12761  9t11e99OLD  12847  decbin2  12859  irec  14237  binom2i  14248  crreczi  14264  3dec  14302  nn0opthi  14306  faclbnd4lem1  14329  rei  15207  imi  15208  iseraltlem2  15734  bpoly3  16112  bpoly4  16113  3dvdsdec  16390  3dvds2dec  16391  odd2np1  16399  gcdaddmlem  16582  3lcm2e6woprm  16673  6lcm4e12  16674  modxai  17128  mod2xnegi  17131  karatsuba  17143  2picn  26588  sinhalfpilem  26594  ef2pi  26608  ef2kpi  26609  efper  26610  sinperlem  26611  sin2kpi  26614  cos2kpi  26615  sin2pim  26616  cos2pim  26617  sincos4thpi  26644  sincos6thpi  26647  pige3ALT  26651  abssinper  26652  efeq1  26659  logi  26718  logneg  26719  logm1  26720  eflogeq  26733  logimul  26745  logneg2  26746  cxpsqrt  26834  root1eq1  26886  cxpeq  26888  ang180lem1  26940  ang180lem3  26942  ang180lem4  26943  1cubrlem  26972  1cubr  26973  quart1lem  26986  asin1  27025  atanlogsublem  27046  log2ublem2  27078  log2ublem3  27079  log2ub  27080  bclbnd  27410  bposlem8  27421  bposlem9  27422  lgsdir2lem5  27459  2lgsoddprmlem3c  27542  2lgsoddprmlem3d  27543  ax5seglem7  29226  ip0i  31118  ip1ilem  31119  ipasslem10  31132  siilem1  31144  normlem0  31402  normlem1  31403  normlem2  31404  normlem3  31405  normlem5  31407  normlem7  31409  bcseqi  31413  norm-ii-i  31430  normpar2i  31449  polid2i  31450  h1de2i  31846  lnopunilem1  32303  lnophmlem2  32310  dfdec100  33115  dpmul100  33157  dp3mul10  33158  dpmul1000  33159  dpexpp1  33168  dpmul  33173  dpmul4  33174  cos9thpiminplylem4  34120  cos9thpiminplylem5  34121  ballotth  34873  efmul2picn  34928  itgexpif  34938  vtscl  34970  circlemeth  34972  hgt750lem  34983  problem2  36091  problem4  36093  quad3  36095  heiborlem6  38389  gcdaddmzz2nncomi  42686  25or6to4  42897  sn-1ne2  42956  sqsumi  42966  sqmid3api  42968  sqdeccom12  42974  cxp112d  43026  cxp111d  43027  cxpi11d  43028  re1m1e0m0  43082  reixi  43108  sn-1ticom  43120  sn-0tie0  43149  proot1ex  43849  areaquad  43869  resqrtvalex  44297  imsqrtvalex  44298  coskpi2  46506  cosnegpi  46507  cosknegpi  46509  wallispilem4  46708  dirkertrigeq  46741  fourierdlem57  46803  fourierdlem62  46808  fourierswlem  46870  cos5t  47539  goldrasin  47542  fmtnorec3  48223  fmtnorec4  48224  lighneallem3  48282  3exp4mod41  48291  41prothprmlem1  48292  zlmodzxzequap  49198  nn0sumshdiglemB  49319  i2linesi  50475