Theorem mulcli 11233

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

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℂcc 11115   · cmul 11122

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcl 11179

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mul02lem2  11404  addrid  11407  cnegex2  11409  ixi  11860  2mulicn  12485  numma  12778  nummac  12779  9t11e99OLD  12865  decbin2  12877  irec  14257  binom2i  14268  crreczi  14284  3dec  14322  nn0opthi  14326  faclbnd4lem1  14349  rei  15233  imi  15234  iseraltlem2  15760  bpoly3  16136  bpoly4  16137  3dvdsdec  16414  3dvds2dec  16415  odd2np1  16423  gcdaddmlem  16606  3lcm2e6woprm  16697  6lcm4e12  16698  modxai  17152  mod2xnegi  17155  karatsuba  17167  2picn  26675  sinhalfpilem  26681  ef2pi  26695  ef2kpi  26696  efper  26697  sinperlem  26698  sin2kpi  26701  cos2kpi  26702  sin2pim  26703  cos2pim  26704  sincos4thpi  26731  sincos6thpi  26734  pige3ALT  26738  abssinper  26739  efeq1  26746  logi  26805  logneg  26806  logm1  26807  eflogeq  26820  logimul  26832  logneg2  26833  cxpsqrt  26921  root1eq1  26973  cxpeq  26975  ang180lem1  27027  ang180lem3  27029  ang180lem4  27030  1cubrlem  27059  1cubr  27060  quart1lem  27073  asin1  27112  atanlogsublem  27133  log2ublem2  27165  log2ublem3  27166  log2ub  27167  bclbnd  27497  bposlem8  27508  bposlem9  27509  lgsdir2lem5  27546  2lgsoddprmlem3c  27629  2lgsoddprmlem3d  27630  ax5seglem7  29342  ip0i  31250  ip1ilem  31251  ipasslem10  31264  siilem1  31276  normlem0  31534  normlem1  31535  normlem2  31536  normlem3  31537  normlem5  31539  normlem7  31541  bcseqi  31545  norm-ii-i  31562  normpar2i  31581  polid2i  31582  h1de2i  31978  lnopunilem1  32435  lnophmlem2  32442  dfdec100  33246  dpmul100  33288  dp3mul10  33289  dpmul1000  33290  dpexpp1  33299  dpmul  33304  dpmul4  33305  cos9thpiminplylem4  34241  cos9thpiminplylem5  34242  ballotth  34995  efmul2picn  35050  itgexpif  35060  vtscl  35092  circlemeth  35094  hgt750lem  35105  problem2  36197  problem4  36199  quad3  36201  heiborlem6  38527  gcdaddmzz2nncomi  42822  25or6to4  43033  sn-1ne2  43092  sqsumi  43102  sqmid3api  43104  sqdeccom12  43110  cxp112d  43162  cxp111d  43163  cxpi11d  43164  re1m1e0m0  43218  reixi  43244  sn-1ticom  43256  sn-0tie0  43285  proot1ex  43983  areaquad  44003  resqrtvalex  44431  imsqrtvalex  44432  coskpi2  46640  cosnegpi  46641  cosknegpi  46643  wallispilem4  46842  dirkertrigeq  46875  fourierdlem57  46937  fourierdlem62  46942  fourierswlem  47004  cos5t  47676  goldrasin  47679  fmtnorec3  48360  fmtnorec4  48361  lighneallem3  48419  3exp4mod41  48428  41prothprmlem1  48429  zlmodzxzequap  49338  nn0sumshdiglemB  49459  i2linesi  50615