Theorem mulcli 10494

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

Syntax hints:   ∈ wcel 2081  (class class class)co 7016  ℂcc 10381   · cmul 10388

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

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

This theorem is referenced by:  mul02lem2  10664  addid1  10667  cnegex2  10669  ixi  11117  2mulicn  11708  numma  11991  nummac  11992  9t11e99  12078  decbin2  12089  irec  13414  binom2i  13424  crreczi  13439  3dec  13476  nn0opthi  13480  faclbnd4lem1  13503  rei  14349  imi  14350  iseraltlem2  14873  bpoly3  15245  bpoly4  15246  3dvdsdec  15514  3dvds2dec  15515  odd2np1  15523  gcdaddmlem  15705  3lcm2e6woprm  15788  6lcm4e12  15789  modxai  16233  mod2xnegi  16236  decexp2  16240  karatsuba  16249  sinhalfpilem  24732  ef2pi  24746  ef2kpi  24747  efper  24748  sinperlem  24749  sin2kpi  24752  cos2kpi  24753  sin2pim  24754  cos2pim  24755  sincos4thpi  24782  sincos6thpi  24784  pige3ALT  24788  abssinper  24789  efeq1  24794  logneg  24852  logm1  24853  eflogeq  24866  logimul  24878  logneg2  24879  cxpsqrt  24967  root1eq1  25017  cxpeq  25019  ang180lem1  25068  ang180lem3  25070  ang180lem4  25071  1cubrlem  25100  1cubr  25101  quart1lem  25114  asin1  25153  atanlogsublem  25174  log2ublem2  25207  log2ublem3  25208  log2ub  25209  bclbnd  25538  bposlem8  25549  bposlem9  25550  lgsdir2lem5  25587  2lgsoddprmlem3c  25670  2lgsoddprmlem3d  25671  ax5seglem7  26404  ip0i  28293  ip1ilem  28294  ipasslem10  28307  siilem1  28319  normlem0  28577  normlem1  28578  normlem2  28579  normlem3  28580  normlem5  28582  normlem7  28584  bcseqi  28588  norm-ii-i  28605  normpar2i  28624  polid2i  28625  h1de2i  29021  lnopunilem1  29478  lnophmlem2  29485  dfdec100  30230  dpmul100  30257  dp3mul10  30258  dpmul1000  30259  dpexpp1  30268  dpmul  30273  dpmul4  30274  ballotth  31412  efmul2picn  31484  itgexpif  31494  vtscl  31526  circlemeth  31528  hgt750lem  31539  problem2  32518  problem4  32520  quad3  32522  logi  32575  heiborlem6  34645  sqsumi  38708  sqmid3api  38710  sqdeccom12  38716  proot1ex  39305  areaquad  39327  coskpi2  41708  cosnegpi  41709  cosknegpi  41711  wallispilem4  41915  dirkerper  41943  dirkertrigeq  41948  dirkercncflem2  41951  fourierdlem57  42010  fourierdlem62  42015  fourierswlem  42077  fmtnorec3  43212  fmtnorec4  43213  lighneallem3  43274  3exp4mod41  43283  41prothprmlem1  43284  zlmodzxzequap  44054  nn0sumshdiglemB  44181  i2linesi  44379