Theorem mulcli 11152

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   · cmul 11043

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

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

This theorem is referenced by:  mul02lem2  11323  addrid  11326  cnegex2  11328  ixi  11779  2mulicn  12401  numma  12688  nummac  12689  9t11e99  12774  decbin2  12785  irec  14163  binom2i  14174  crreczi  14190  3dec  14228  nn0opthi  14232  faclbnd4lem1  14255  rei  15118  imi  15119  iseraltlem2  15645  bpoly3  16023  bpoly4  16024  3dvdsdec  16301  3dvds2dec  16302  odd2np1  16310  gcdaddmlem  16493  3lcm2e6woprm  16584  6lcm4e12  16585  modxai  17039  mod2xnegi  17042  karatsuba  17054  sinhalfpilem  26427  ef2pi  26441  ef2kpi  26442  efper  26443  sinperlem  26444  sin2kpi  26447  cos2kpi  26448  sin2pim  26449  cos2pim  26450  sincos4thpi  26477  sincos6thpi  26480  pige3ALT  26484  abssinper  26485  efeq1  26492  logi  26551  logneg  26552  logm1  26553  eflogeq  26566  logimul  26578  logneg2  26579  cxpsqrt  26667  root1eq1  26719  cxpeq  26721  ang180lem1  26773  ang180lem3  26775  ang180lem4  26776  1cubrlem  26805  1cubr  26806  quart1lem  26819  asin1  26858  atanlogsublem  26879  log2ublem2  26911  log2ublem3  26912  log2ub  26913  bclbnd  27243  bposlem8  27254  bposlem9  27255  lgsdir2lem5  27292  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  ax5seglem7  29004  ip0i  30896  ip1ilem  30897  ipasslem10  30910  siilem1  30922  normlem0  31180  normlem1  31181  normlem2  31182  normlem3  31183  normlem5  31185  normlem7  31187  bcseqi  31191  norm-ii-i  31208  normpar2i  31227  polid2i  31228  h1de2i  31624  lnopunilem1  32081  lnophmlem2  32088  dfdec100  32903  dpmul100  32956  dp3mul10  32957  dpmul1000  32958  dpexpp1  32967  dpmul  32972  dpmul4  32973  cos9thpiminplylem4  33929  cos9thpiminplylem5  33930  ballotth  34682  efmul2picn  34740  itgexpif  34750  vtscl  34782  circlemeth  34784  hgt750lem  34795  problem2  35848  problem4  35850  quad3  35852  heiborlem6  38137  gcdaddmzz2nncomi  42434  sn-1ne2  42703  sqsumi  42713  sqmid3api  42715  sqdeccom12  42721  cxp112d  42773  cxp111d  42774  cxpi11d  42775  re1m1e0m0  42829  reixi  42855  sn-1ticom  42867  sn-0tie0  42896  proot1ex  43624  areaquad  43644  resqrtvalex  44072  imsqrtvalex  44073  coskpi2  46294  cosnegpi  46295  cosknegpi  46297  wallispilem4  46496  dirkerper  46524  dirkertrigeq  46529  dirkercncflem2  46532  fourierdlem57  46591  fourierdlem62  46596  fourierswlem  46658  cos5t  47327  goldrasin  47330  fmtnorec3  48011  fmtnorec4  48012  lighneallem3  48070  3exp4mod41  48079  41prothprmlem1  48080  zlmodzxzequap  48975  nn0sumshdiglemB  49096  i2linesi  50253