Theorem mulcli 9924

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

Syntax hints:   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   · cmul 9820

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

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  mul02lem2  10092  addid1  10095  cnegex2  10097  ixi  10535  2mulicn  11132  numma  11433  nummac  11434  9t11e99  11547  9t11e99OLD  11548  decbin2  11559  irec  12826  binom2i  12836  crreczi  12851  3dec  12912  sq10OLD  12913  3decOLD  12915  nn0opthi  12919  faclbnd4lem1  12942  rei  13744  imi  13745  iseraltlem2  14261  bpoly3  14628  bpoly4  14629  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  odd2np1  14903  gcdaddmlem  15083  3lcm2e6woprm  15166  6lcm4e12  15167  modxai  15610  mod2xnegi  15613  decexp2  15617  decsplitOLD  15629  karatsuba  15630  karatsubaOLD  15631  sinhalfpilem  24019  ef2pi  24033  ef2kpi  24034  efper  24035  sinperlem  24036  sin2kpi  24039  cos2kpi  24040  sin2pim  24041  cos2pim  24042  sincos4thpi  24069  sincos6thpi  24071  pige3  24073  abssinper  24074  efeq1  24079  logneg  24138  logm1  24139  eflogeq  24152  logimul  24164  logneg2  24165  cxpsqrt  24249  root1eq1  24296  cxpeq  24298  ang180lem1  24339  ang180lem3  24341  ang180lem4  24342  1cubrlem  24368  1cubr  24369  quart1lem  24382  asin1  24421  atanlogsublem  24442  log2ublem2  24474  log2ublem3  24475  log2ub  24476  bclbnd  24805  bposlem8  24816  bposlem9  24817  lgsdir2lem5  24854  2lgsoddprmlem3c  24937  2lgsoddprmlem3d  24938  ax5seglem7  25615  ip0i  27064  ip1ilem  27065  ipasslem10  27078  siilem1  27090  normlem0  27350  normlem1  27351  normlem2  27352  normlem3  27353  normlem5  27355  normlem7  27357  bcseqi  27361  norm-ii-i  27378  normpar2i  27397  polid2i  27398  h1de2i  27796  lnopunilem1  28253  lnophmlem2  28260  ballotth  29926  problem2  30813  problem2OLD  30814  problem4  30816  quad3  30818  logi  30873  heiborlem6  32785  proot1ex  36798  areaquad  36821  coskpi2  38749  cosnegpi  38750  cosknegpi  38752  wallispilem4  38961  dirkerper  38989  dirkertrigeq  38994  dirkercncflem2  38997  fourierdlem57  39056  fourierdlem62  39061  fourierswlem  39123  fmtnorec3  39998  fmtnorec4  39999  lighneallem3  40062  3exp4mod41  40071  41prothprmlem1  40072  zlmodzxzequap  42082  nn0sumshdiglemB  42212  i2linesi  42333