Theorem mulcli 11271

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

Syntax hints:   ∈ wcel 2099  (class class class)co 7424  ℂcc 11156   · cmul 11163

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

This theorem depends on definitions:  df-bi 206  df-an 395

This theorem is referenced by:  mul02lem2  11441  addrid  11444  cnegex2  11446  ixi  11893  2mulicn  12487  numma  12773  nummac  12774  9t11e99  12859  decbin2  12870  irec  14219  binom2i  14230  crreczi  14245  3dec  14283  nn0opthi  14287  faclbnd4lem1  14310  rei  15161  imi  15162  iseraltlem2  15687  bpoly3  16060  bpoly4  16061  3dvdsdec  16334  3dvds2dec  16335  odd2np1  16343  gcdaddmlem  16524  3lcm2e6woprm  16616  6lcm4e12  16617  modxai  17070  mod2xnegi  17073  decexp2  17077  karatsuba  17086  sinhalfpilem  26491  ef2pi  26505  ef2kpi  26506  efper  26507  sinperlem  26508  sin2kpi  26511  cos2kpi  26512  sin2pim  26513  cos2pim  26514  sincos4thpi  26541  sincos6thpi  26543  pige3ALT  26547  abssinper  26548  efeq1  26555  logi  26614  logneg  26615  logm1  26616  eflogeq  26629  logimul  26641  logneg2  26642  cxpsqrt  26730  root1eq1  26783  cxpeq  26785  ang180lem1  26837  ang180lem3  26839  ang180lem4  26840  1cubrlem  26869  1cubr  26870  quart1lem  26883  asin1  26922  atanlogsublem  26943  log2ublem2  26975  log2ublem3  26976  log2ub  26977  bclbnd  27309  bposlem8  27320  bposlem9  27321  lgsdir2lem5  27358  2lgsoddprmlem3c  27441  2lgsoddprmlem3d  27442  ax5seglem7  28869  ip0i  30758  ip1ilem  30759  ipasslem10  30772  siilem1  30784  normlem0  31042  normlem1  31043  normlem2  31044  normlem3  31045  normlem5  31047  normlem7  31049  bcseqi  31053  norm-ii-i  31070  normpar2i  31089  polid2i  31090  h1de2i  31486  lnopunilem1  31943  lnophmlem2  31950  dfdec100  32731  dpmul100  32758  dp3mul10  32759  dpmul1000  32760  dpexpp1  32769  dpmul  32774  dpmul4  32775  ballotth  34371  efmul2picn  34442  itgexpif  34452  vtscl  34484  circlemeth  34486  hgt750lem  34497  problem2  35494  problem4  35496  quad3  35498  heiborlem6  37517  gcdaddmzz2nncomi  41694  sn-1ne2  42079  sqsumi  42094  sqmid3api  42096  sqdeccom12  42102  cxp112d  42137  cxp111d  42138  cxpi11d  42139  re1m1e0m0  42177  reixi  42202  sn-1ticom  42214  sn-0tie0  42219  sn-inelr  42247  proot1ex  42861  areaquad  42881  resqrtvalex  43312  imsqrtvalex  43313  coskpi2  45487  cosnegpi  45488  cosknegpi  45490  wallispilem4  45689  dirkerper  45717  dirkertrigeq  45722  dirkercncflem2  45725  fourierdlem57  45784  fourierdlem62  45789  fourierswlem  45851  fmtnorec3  47120  fmtnorec4  47121  lighneallem3  47179  3exp4mod41  47188  41prothprmlem1  47189  zlmodzxzequap  47882  nn0sumshdiglemB  48008  i2linesi  48526