Theorem mulcli 11211

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

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   · cmul 11100

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

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

This theorem is referenced by:  mul02lem2  11382  addrid  11385  cnegex2  11387  ixi  11838  2mulicn  12463  numma  12755  nummac  12756  9t11e99OLD  12842  decbin2  12854  irec  14233  binom2i  14244  crreczi  14260  3dec  14298  nn0opthi  14302  faclbnd4lem1  14325  rei  15203  imi  15204  iseraltlem2  15730  bpoly3  16107  bpoly4  16108  3dvdsdec  16385  3dvds2dec  16386  odd2np1  16394  gcdaddmlem  16577  3lcm2e6woprm  16668  6lcm4e12  16669  modxai  17123  mod2xnegi  17126  karatsuba  17138  2picn  26622  sinhalfpilem  26628  ef2pi  26642  ef2kpi  26643  efper  26644  sinperlem  26645  sin2kpi  26648  cos2kpi  26649  sin2pim  26650  cos2pim  26651  sincos4thpi  26678  sincos6thpi  26681  pige3ALT  26685  abssinper  26686  efeq1  26693  logi  26752  logneg  26753  logm1  26754  eflogeq  26767  logimul  26779  logneg2  26780  cxpsqrt  26868  root1eq1  26920  cxpeq  26922  ang180lem1  26974  ang180lem3  26976  ang180lem4  26977  1cubrlem  27006  1cubr  27007  quart1lem  27020  asin1  27059  atanlogsublem  27080  log2ublem2  27112  log2ublem3  27113  log2ub  27114  bclbnd  27444  bposlem8  27455  bposlem9  27456  lgsdir2lem5  27493  2lgsoddprmlem3c  27576  2lgsoddprmlem3d  27577  ax5seglem7  29285  ip0i  31177  ip1ilem  31178  ipasslem10  31191  siilem1  31203  normlem0  31461  normlem1  31462  normlem2  31463  normlem3  31464  normlem5  31466  normlem7  31468  bcseqi  31472  norm-ii-i  31489  normpar2i  31508  polid2i  31509  h1de2i  31905  lnopunilem1  32362  lnophmlem2  32369  dfdec100  33174  dpmul100  33216  dp3mul10  33217  dpmul1000  33218  dpexpp1  33227  dpmul  33232  dpmul4  33233  cos9thpiminplylem4  34175  cos9thpiminplylem5  34176  ballotth  34928  efmul2picn  34983  itgexpif  34993  vtscl  35025  circlemeth  35027  hgt750lem  35038  problem2  36158  problem4  36160  quad3  36162  heiborlem6  38487  gcdaddmzz2nncomi  42782  25or6to4  42993  sn-1ne2  43052  sqsumi  43062  sqmid3api  43064  sqdeccom12  43070  cxp112d  43122  cxp111d  43123  cxpi11d  43124  re1m1e0m0  43178  reixi  43204  sn-1ticom  43216  sn-0tie0  43245  proot1ex  43943  areaquad  43963  resqrtvalex  44391  imsqrtvalex  44392  coskpi2  46600  cosnegpi  46601  cosknegpi  46603  wallispilem4  46802  dirkertrigeq  46835  fourierdlem57  46897  fourierdlem62  46902  fourierswlem  46964  cos5t  47636  goldrasin  47639  fmtnorec3  48320  fmtnorec4  48321  lighneallem3  48379  3exp4mod41  48388  41prothprmlem1  48389  zlmodzxzequap  49299  nn0sumshdiglemB  49420  i2linesi  50576  crossp3i  50668