Theorem mulcl 8001

Description: Alias for ax-mulcl 7972, for naming consistency with mulcli 8026. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
mulcl	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Proof of Theorem mulcl

Step	Hyp	Ref	Expression
1		ax-mulcl 7972	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   · cmul 7879

This theorem was proved from axioms:  ax-mulcl 7972

This theorem is referenced by:  mpomulf  8011  0cn  8013  mulrid  8018  mulcli  8026  mulcld  8042  mul31  8152  mul4  8153  muladd11r  8177  cnegexlem2  8197  cnegex  8199  muladd  8405  subdi  8406  mul02  8408  submul2  8420  mulsub  8422  recextlem1  8672  recexap  8674  muleqadd  8689  divassap  8711  divmulassap  8716  divmuldivap  8733  divmuleqap  8738  divadddivap  8748  conjmulap  8750  cju  8982  ofnegsub  8983  zneo  9421  exp3vallem  10614  exp3val  10615  exp1  10619  expp1  10620  expcl  10631  expclzaplem  10637  mulexp  10652  sqcl  10674  subsq  10720  subsq2  10721  binom2sub  10727  mulbinom2  10730  binom3  10731  zesq  10732  bernneq  10734  bernneq2  10735  mulsubdivbinom2ap  10785  facnn  10801  fac0  10802  fac1  10803  facp1  10804  bcval5  10837  bcn2  10838  reim  10999  imcl  11001  crre  11004  crim  11005  remim  11007  mulreap  11011  cjreb  11013  recj  11014  reneg  11015  readd  11016  remullem  11018  remul2  11020  imcj  11022  imneg  11023  imadd  11024  immul2  11027  cjadd  11031  ipcnval  11033  cjmulrcl  11034  cjneg  11037  imval2  11041  cjreim  11050  rennim  11149  sqabsadd  11202  sqabssub  11203  absreimsq  11214  absreim  11215  absmul  11216  mul0inf  11387  mulcn2  11458  climmul  11473  isermulc2  11486  fsummulc2  11594  prodf  11684  clim2prod  11685  clim2divap  11686  prod3fmul  11687  prodf1  11688  prodfap0  11691  prodfrecap  11692  prodrbdclem  11717  fproddccvg  11718  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  fprodntrivap  11730  prodsnf  11738  fprodcl  11753  fprodclf  11781  efexp  11828  sinf  11850  cosf  11851  tanval2ap  11859  tanval3ap  11860  resinval  11861  recosval  11862  efi4p  11863  resin4p  11864  recos4p  11865  resincl  11866  recoscl  11867  sinneg  11872  cosneg  11873  efival  11878  efmival  11879  efeul  11880  sinadd  11882  cosadd  11883  sinsub  11886  cossub  11887  subsin  11889  sinmul  11890  cosmul  11891  addcos  11892  subcos  11893  cos2tsin  11897  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  absef  11916  absefib  11917  efieq1re  11918  demoivre  11919  demoivreALT  11920  odd2np1lem  12016  odd2np1  12017  opoe  12039  omoe  12040  opeo  12041  omeo  12042  modgcd  12131  qredeq  12237  modprm0  12395  pythagtriplem1  12406  pythagtriplem12  12416  pythagtriplem14  12418  gzmulcl  12519  4sqlem11  12542  4sqlem17  12548  cncrng  14068  cnfldmulg  14075  mpomulcn  14745  mulc1cncf  14768  mulcncflem  14786  dvmulxxbr  14881  dvmulxx  14883  dvimulf  14885  plymullem1  14927  plymulcl  14934  plysubcl  14935  efper  14983  sinperlem  14984  sin2kpi  14987  cos2kpi  14988  efimpi  14995  sincosq1eq  15015  abssinper  15022  sinkpi  15023  coskpi  15024  binom4  15152  lgsdilem2  15193  lgsne0  15195  lgsquadlem1  15234  2sqlem2  15272