Theorem mulcli 11293

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

Syntax hints:   ∈ wcel 2103  (class class class)co 7445  ℂcc 11178   · cmul 11185

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

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

This theorem is referenced by:  mul02lem2  11463  addrid  11466  cnegex2  11468  ixi  11915  2mulicn  12512  numma  12798  nummac  12799  9t11e99  12884  decbin2  12895  irec  14246  binom2i  14257  crreczi  14273  3dec  14311  nn0opthi  14315  faclbnd4lem1  14338  rei  15201  imi  15202  iseraltlem2  15727  bpoly3  16100  bpoly4  16101  3dvdsdec  16374  3dvds2dec  16375  odd2np1  16383  gcdaddmlem  16564  3lcm2e6woprm  16656  6lcm4e12  16657  modxai  17110  mod2xnegi  17113  decexp2  17117  karatsuba  17126  sinhalfpilem  26515  ef2pi  26529  ef2kpi  26530  efper  26531  sinperlem  26532  sin2kpi  26535  cos2kpi  26536  sin2pim  26537  cos2pim  26538  sincos4thpi  26565  sincos6thpi  26567  pige3ALT  26571  abssinper  26572  efeq1  26579  logi  26638  logneg  26639  logm1  26640  eflogeq  26653  logimul  26665  logneg2  26666  cxpsqrt  26754  root1eq1  26807  cxpeq  26809  ang180lem1  26861  ang180lem3  26863  ang180lem4  26864  1cubrlem  26893  1cubr  26894  quart1lem  26907  asin1  26946  atanlogsublem  26967  log2ublem2  26999  log2ublem3  27000  log2ub  27001  bclbnd  27333  bposlem8  27344  bposlem9  27345  lgsdir2lem5  27382  2lgsoddprmlem3c  27465  2lgsoddprmlem3d  27466  ax5seglem7  28959  ip0i  30848  ip1ilem  30849  ipasslem10  30862  siilem1  30874  normlem0  31132  normlem1  31133  normlem2  31134  normlem3  31135  normlem5  31137  normlem7  31139  bcseqi  31143  norm-ii-i  31160  normpar2i  31179  polid2i  31180  h1de2i  31576  lnopunilem1  32033  lnophmlem2  32040  dfdec100  32826  dpmul100  32853  dp3mul10  32854  dpmul1000  32855  dpexpp1  32864  dpmul  32869  dpmul4  32870  ballotth  34494  efmul2picn  34565  itgexpif  34575  vtscl  34607  circlemeth  34609  hgt750lem  34620  problem2  35626  problem4  35628  quad3  35630  heiborlem6  37724  gcdaddmzz2nncomi  41900  sn-1ne2  42202  sqsumi  42218  sqmid3api  42220  sqdeccom12  42226  cxp112d  42266  cxp111d  42267  cxpi11d  42268  re1m1e0m0  42306  reixi  42331  sn-1ticom  42343  sn-0tie0  42348  sn-inelr  42376  proot1ex  43097  areaquad  43117  resqrtvalex  43547  imsqrtvalex  43548  coskpi2  45721  cosnegpi  45722  cosknegpi  45724  wallispilem4  45923  dirkerper  45951  dirkertrigeq  45956  dirkercncflem2  45959  fourierdlem57  46018  fourierdlem62  46023  fourierswlem  46085  fmtnorec3  47354  fmtnorec4  47355  lighneallem3  47413  3exp4mod41  47422  41prothprmlem1  47423  zlmodzxzequap  48146  nn0sumshdiglemB  48272  i2linesi  48790