Theorem mulcli 11146

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030   · cmul 11037

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mul02lem2  11317  addrid  11320  cnegex2  11322  ixi  11773  2mulicn  12395  numma  12682  nummac  12683  9t11e99  12768  decbin2  12779  irec  14157  binom2i  14168  crreczi  14184  3dec  14222  nn0opthi  14226  faclbnd4lem1  14249  rei  15112  imi  15113  iseraltlem2  15639  bpoly3  16017  bpoly4  16018  3dvdsdec  16295  3dvds2dec  16296  odd2np1  16304  gcdaddmlem  16487  3lcm2e6woprm  16578  6lcm4e12  16579  modxai  17033  mod2xnegi  17036  karatsuba  17048  sinhalfpilem  26443  ef2pi  26457  ef2kpi  26458  efper  26459  sinperlem  26460  sin2kpi  26463  cos2kpi  26464  sin2pim  26465  cos2pim  26466  sincos4thpi  26493  sincos6thpi  26496  pige3ALT  26500  abssinper  26501  efeq1  26508  logi  26567  logneg  26568  logm1  26569  eflogeq  26582  logimul  26594  logneg2  26595  cxpsqrt  26683  root1eq1  26735  cxpeq  26737  ang180lem1  26789  ang180lem3  26791  ang180lem4  26792  1cubrlem  26821  1cubr  26822  quart1lem  26835  asin1  26874  atanlogsublem  26895  log2ublem2  26927  log2ublem3  26928  log2ub  26929  bclbnd  27260  bposlem8  27271  bposlem9  27272  lgsdir2lem5  27309  2lgsoddprmlem3c  27392  2lgsoddprmlem3d  27393  ax5seglem7  29021  ip0i  30914  ip1ilem  30915  ipasslem10  30928  siilem1  30940  normlem0  31198  normlem1  31199  normlem2  31200  normlem3  31201  normlem5  31203  normlem7  31205  bcseqi  31209  norm-ii-i  31226  normpar2i  31245  polid2i  31246  h1de2i  31642  lnopunilem1  32099  lnophmlem2  32106  dfdec100  32921  dpmul100  32974  dp3mul10  32975  dpmul1000  32976  dpexpp1  32985  dpmul  32990  dpmul4  32991  cos9thpiminplylem4  33948  cos9thpiminplylem5  33949  ballotth  34701  efmul2picn  34759  itgexpif  34769  vtscl  34801  circlemeth  34803  hgt750lem  34814  problem2  35867  problem4  35869  quad3  35871  heiborlem6  38154  gcdaddmzz2nncomi  42451  sn-1ne2  42720  sqsumi  42730  sqmid3api  42732  sqdeccom12  42738  cxp112d  42790  cxp111d  42791  cxpi11d  42792  re1m1e0m0  42846  reixi  42872  sn-1ticom  42884  sn-0tie0  42913  proot1ex  43645  areaquad  43665  resqrtvalex  44093  imsqrtvalex  44094  coskpi2  46315  cosnegpi  46316  cosknegpi  46318  wallispilem4  46517  dirkerper  46545  dirkertrigeq  46550  dirkercncflem2  46553  fourierdlem57  46612  fourierdlem62  46617  fourierswlem  46679  goldrasin  47347  fmtnorec3  48026  fmtnorec4  48027  lighneallem3  48085  3exp4mod41  48094  41prothprmlem1  48095  zlmodzxzequap  48990  nn0sumshdiglemB  49111  i2linesi  50268