Theorem mulcli 10991

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

Syntax hints:   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878   · cmul 10885

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

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

This theorem is referenced by:  mul02lem2  11161  addid1  11164  cnegex2  11166  ixi  11613  2mulicn  12205  numma  12490  nummac  12491  9t11e99  12576  decbin2  12587  irec  13927  binom2i  13937  crreczi  13952  3dec  13989  nn0opthi  13993  faclbnd4lem1  14016  rei  14876  imi  14877  iseraltlem2  15403  bpoly3  15777  bpoly4  15778  3dvdsdec  16050  3dvds2dec  16051  odd2np1  16059  gcdaddmlem  16240  3lcm2e6woprm  16329  6lcm4e12  16330  modxai  16778  mod2xnegi  16781  decexp2  16785  karatsuba  16794  sinhalfpilem  25629  ef2pi  25643  ef2kpi  25644  efper  25645  sinperlem  25646  sin2kpi  25649  cos2kpi  25650  sin2pim  25651  cos2pim  25652  sincos4thpi  25679  sincos6thpi  25681  pige3ALT  25685  abssinper  25686  efeq1  25693  logneg  25752  logm1  25753  eflogeq  25766  logimul  25778  logneg2  25779  cxpsqrt  25867  root1eq1  25917  cxpeq  25919  ang180lem1  25968  ang180lem3  25970  ang180lem4  25971  1cubrlem  26000  1cubr  26001  quart1lem  26014  asin1  26053  atanlogsublem  26074  log2ublem2  26106  log2ublem3  26107  log2ub  26108  bclbnd  26437  bposlem8  26448  bposlem9  26449  lgsdir2lem5  26486  2lgsoddprmlem3c  26569  2lgsoddprmlem3d  26570  ax5seglem7  27312  ip0i  29196  ip1ilem  29197  ipasslem10  29210  siilem1  29222  normlem0  29480  normlem1  29481  normlem2  29482  normlem3  29483  normlem5  29485  normlem7  29487  bcseqi  29491  norm-ii-i  29508  normpar2i  29527  polid2i  29528  h1de2i  29924  lnopunilem1  30381  lnophmlem2  30388  dfdec100  31153  dpmul100  31180  dp3mul10  31181  dpmul1000  31182  dpexpp1  31191  dpmul  31196  dpmul4  31197  ballotth  32513  efmul2picn  32585  itgexpif  32595  vtscl  32627  circlemeth  32629  hgt750lem  32640  problem2  33633  problem4  33635  quad3  33637  logi  33709  heiborlem6  35983  gcdaddmzz2nncomi  40011  sn-1ne2  40302  sqsumi  40316  sqmid3api  40318  sqdeccom12  40324  re1m1e0m0  40387  reixi  40411  sn-1ticom  40423  sn-0tie0  40428  sn-inelr  40442  proot1ex  41033  areaquad  41054  resqrtvalex  41260  imsqrtvalex  41261  coskpi2  43414  cosnegpi  43415  cosknegpi  43417  wallispilem4  43616  dirkerper  43644  dirkertrigeq  43649  dirkercncflem2  43652  fourierdlem57  43711  fourierdlem62  43716  fourierswlem  43778  fmtnorec3  45011  fmtnorec4  45012  lighneallem3  45070  3exp4mod41  45079  41prothprmlem1  45080  zlmodzxzequap  45851  nn0sumshdiglemB  45977  i2linesi  46493