Theorem mulcli 11141

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

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℂcc 11026   · cmul 11033

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

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

This theorem is referenced by:  mul02lem2  11312  addrid  11315  cnegex2  11317  ixi  11768  2mulicn  12367  numma  12653  nummac  12654  9t11e99  12739  decbin2  12750  irec  14126  binom2i  14137  crreczi  14153  3dec  14191  nn0opthi  14195  faclbnd4lem1  14218  rei  15081  imi  15082  iseraltlem2  15608  bpoly3  15983  bpoly4  15984  3dvdsdec  16261  3dvds2dec  16262  odd2np1  16270  gcdaddmlem  16453  3lcm2e6woprm  16544  6lcm4e12  16545  modxai  16998  mod2xnegi  17001  karatsuba  17013  sinhalfpilem  26430  ef2pi  26444  ef2kpi  26445  efper  26446  sinperlem  26447  sin2kpi  26450  cos2kpi  26451  sin2pim  26452  cos2pim  26453  sincos4thpi  26480  sincos6thpi  26483  pige3ALT  26487  abssinper  26488  efeq1  26495  logi  26554  logneg  26555  logm1  26556  eflogeq  26569  logimul  26581  logneg2  26582  cxpsqrt  26670  root1eq1  26723  cxpeq  26725  ang180lem1  26777  ang180lem3  26779  ang180lem4  26780  1cubrlem  26809  1cubr  26810  quart1lem  26823  asin1  26862  atanlogsublem  26883  log2ublem2  26915  log2ublem3  26916  log2ub  26917  bclbnd  27249  bposlem8  27260  bposlem9  27261  lgsdir2lem5  27298  2lgsoddprmlem3c  27381  2lgsoddprmlem3d  27382  ax5seglem7  29010  ip0i  30902  ip1ilem  30903  ipasslem10  30916  siilem1  30928  normlem0  31186  normlem1  31187  normlem2  31188  normlem3  31189  normlem5  31191  normlem7  31193  bcseqi  31197  norm-ii-i  31214  normpar2i  31233  polid2i  31234  h1de2i  31630  lnopunilem1  32087  lnophmlem2  32094  dfdec100  32913  dpmul100  32980  dp3mul10  32981  dpmul1000  32982  dpexpp1  32991  dpmul  32996  dpmul4  32997  cos9thpiminplylem4  33944  cos9thpiminplylem5  33945  ballotth  34697  efmul2picn  34755  itgexpif  34765  vtscl  34797  circlemeth  34799  hgt750lem  34810  problem2  35862  problem4  35864  quad3  35866  heiborlem6  38019  gcdaddmzz2nncomi  42271  sn-1ne2  42541  sqsumi  42557  sqmid3api  42559  sqdeccom12  42565  cxp112d  42617  cxp111d  42618  cxpi11d  42619  re1m1e0m0  42673  reixi  42699  sn-1ticom  42711  sn-0tie0  42727  proot1ex  43459  areaquad  43479  resqrtvalex  43907  imsqrtvalex  43908  coskpi2  46131  cosnegpi  46132  cosknegpi  46134  wallispilem4  46333  dirkerper  46361  dirkertrigeq  46366  dirkercncflem2  46369  fourierdlem57  46428  fourierdlem62  46433  fourierswlem  46495  fmtnorec3  47815  fmtnorec4  47816  lighneallem3  47874  3exp4mod41  47883  41prothprmlem1  47884  zlmodzxzequap  48766  nn0sumshdiglemB  48887  i2linesi  50044