Theorem mulcli 11243

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

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℂcc 11125   · cmul 11132

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

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

This theorem is used by:  mul02lem2  11414  addrid  11417  cnegex2  11419  ixi  11870  2mulicn  12495  numma  12788  nummac  12789  9t11e99OLD  12875  decbin2  12887  irec  14268  binom2i  14279  crreczi  14295  3dec  14333  nn0opthi  14337  faclbnd4lem1  14360  rei  15246  imi  15247  iseraltlem2  15773  bpoly3  16147  bpoly4  16148  3dvdsdec  16425  3dvds2dec  16426  odd2np1  16434  gcdaddmlem  16617  3lcm2e6woprm  16708  6lcm4e12  16709  modxai  17163  mod2xnegi  17166  karatsuba  17178  2picn  26698  sinhalfpilem  26704  ef2pi  26718  ef2kpi  26719  efper  26720  sinperlem  26721  sin2kpi  26724  cos2kpi  26725  sin2pim  26726  cos2pim  26727  sincos4thpi  26754  sincos6thpi  26756  pige3ALT  26760  abssinper  26761  efeq1  26768  logi  26827  logneg  26828  logm1  26829  eflogeq  26842  logimul  26854  logneg2  26855  cxpsqrt  26943  root1eq1  26995  cxpeq  26997  ang180lem1  27049  ang180lem3  27051  ang180lem4  27052  1cubrlem  27081  1cubr  27082  quart1lem  27095  asin1  27134  atanlogsublem  27155  log2ublem2  27187  log2ublem3  27188  log2ub  27189  bclbnd  27519  bposlem8  27530  bposlem9  27531  lgsdir2lem5  27568  2lgsoddprmlem3c  27651  2lgsoddprmlem3d  27652  ax5seglem7  29395  ip0i  31309  ip1ilem  31310  ipasslem10  31323  siilem1  31335  normlem0  31593  normlem1  31594  normlem2  31595  normlem3  31596  normlem5  31598  normlem7  31600  bcseqi  31604  norm-ii-i  31621  normpar2i  31640  polid2i  31641  h1de2i  32037  lnopunilem1  32494  lnophmlem2  32501  dfdec100  33303  dpmul100  33345  dp3mul10  33346  dpmul1000  33347  dpexpp1  33356  dpmul  33361  dpmul4  33362  cos9thpiminplylem4  34298  cos9thpiminplylem5  34299  ballotth  35052  efmul2picn  35107  itgexpif  35117  vtscl  35149  circlemeth  35151  hgt750lem  35162  problem2  36248  problem4  36250  quad3  36252  heiborlem6  38569  gcdaddmzz2nncomi  42864  25or6to4  43075  sn-1ne2  43149  sqsumi  43159  sqmid3api  43161  sqdeccom12  43167  cxp112d  43219  cxp111d  43220  cxpi11d  43221  re1m1e0m0  43275  reixi  43301  sn-1ticom  43313  sn-0tie0  43342  proot1ex  44040  areaquad  44060  resqrtvalex  44488  imsqrtvalex  44489  coskpi2  46697  cosnegpi  46698  cosknegpi  46700  wallispilem4  46899  dirkertrigeq  46932  fourierdlem57  46994  fourierdlem62  46999  fourierswlem  47061  cos5t  47746  goldpolyfactor  47748  goldrasin  47750  goldratmolem3  47755  goldratmolem4  47756  fmtnorec3  48454  fmtnorec4  48455  lighneallem3  48513  3exp4mod41  48522  41prothprmlem1  48523  zlmodzxzequap  49432  nn0sumshdiglemB  49553  i2linesi  50710