Theorem mulcli 10648

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   · cmul 10542

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  mul02lem2  10817  addid1  10820  cnegex2  10822  ixi  11269  2mulicn  11861  numma  12143  nummac  12144  9t11e99  12229  decbin2  12240  irec  13565  binom2i  13575  crreczi  13590  3dec  13627  nn0opthi  13631  faclbnd4lem1  13654  rei  14515  imi  14516  iseraltlem2  15039  bpoly3  15412  bpoly4  15413  3dvdsdec  15681  3dvds2dec  15682  odd2np1  15690  gcdaddmlem  15872  3lcm2e6woprm  15959  6lcm4e12  15960  modxai  16404  mod2xnegi  16407  decexp2  16411  karatsuba  16420  sinhalfpilem  25049  ef2pi  25063  ef2kpi  25064  efper  25065  sinperlem  25066  sin2kpi  25069  cos2kpi  25070  sin2pim  25071  cos2pim  25072  sincos4thpi  25099  sincos6thpi  25101  pige3ALT  25105  abssinper  25106  efeq1  25113  logneg  25171  logm1  25172  eflogeq  25185  logimul  25197  logneg2  25198  cxpsqrt  25286  root1eq1  25336  cxpeq  25338  ang180lem1  25387  ang180lem3  25389  ang180lem4  25390  1cubrlem  25419  1cubr  25420  quart1lem  25433  asin1  25472  atanlogsublem  25493  log2ublem2  25525  log2ublem3  25526  log2ub  25527  bclbnd  25856  bposlem8  25867  bposlem9  25868  lgsdir2lem5  25905  2lgsoddprmlem3c  25988  2lgsoddprmlem3d  25989  ax5seglem7  26721  ip0i  28602  ip1ilem  28603  ipasslem10  28616  siilem1  28628  normlem0  28886  normlem1  28887  normlem2  28888  normlem3  28889  normlem5  28891  normlem7  28893  bcseqi  28897  norm-ii-i  28914  normpar2i  28933  polid2i  28934  h1de2i  29330  lnopunilem1  29787  lnophmlem2  29794  dfdec100  30546  dpmul100  30573  dp3mul10  30574  dpmul1000  30575  dpexpp1  30584  dpmul  30589  dpmul4  30590  ballotth  31795  efmul2picn  31867  itgexpif  31877  vtscl  31909  circlemeth  31911  hgt750lem  31922  problem2  32909  problem4  32911  quad3  32913  logi  32966  heiborlem6  35109  gcdaddmzz2nncomi  39122  sn-1ne2  39207  sqsumi  39216  sqmid3api  39218  sqdeccom12  39224  re1m1e0m0  39276  proot1ex  39850  areaquad  39872  coskpi2  42196  cosnegpi  42197  cosknegpi  42199  wallispilem4  42402  dirkerper  42430  dirkertrigeq  42435  dirkercncflem2  42438  fourierdlem57  42497  fourierdlem62  42502  fourierswlem  42564  fmtnorec3  43759  fmtnorec4  43760  lighneallem3  43821  3exp4mod41  43830  41prothprmlem1  43831  zlmodzxzequap  44603  nn0sumshdiglemB  44729  i2linesi  44928