Theorem mulcl 8023

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  (class class class)co 5925  ℂcc 7894   · cmul 7901

This theorem was proved from axioms:  ax-mulcl 7994

This theorem is referenced by:  mpomulf  8033  0cn  8035  mulrid  8040  mulcli  8048  mulcld  8064  mul31  8174  mul4  8175  muladd11r  8199  cnegexlem2  8219  cnegex  8221  muladd  8427  subdi  8428  mul02  8430  submul2  8442  mulsub  8444  recextlem1  8695  recexap  8697  muleqadd  8712  divassap  8734  divmulassap  8739  divmuldivap  8756  divmuleqap  8761  divadddivap  8771  conjmulap  8773  cju  9005  ofnegsub  9006  zneo  9444  exp3vallem  10649  exp3val  10650  exp1  10654  expp1  10655  expcl  10666  expclzaplem  10672  mulexp  10687  sqcl  10709  subsq  10755  subsq2  10756  binom2sub  10762  mulbinom2  10765  binom3  10766  zesq  10767  bernneq  10769  bernneq2  10770  mulsubdivbinom2ap  10820  facnn  10836  fac0  10837  fac1  10838  facp1  10839  bcval5  10872  bcn2  10873  reim  11034  imcl  11036  crre  11039  crim  11040  remim  11042  mulreap  11046  cjreb  11048  recj  11049  reneg  11050  readd  11051  remullem  11053  remul2  11055  imcj  11057  imneg  11058  imadd  11059  immul2  11062  cjadd  11066  ipcnval  11068  cjmulrcl  11069  cjneg  11072  imval2  11076  cjreim  11085  rennim  11184  sqabsadd  11237  sqabssub  11238  absreimsq  11249  absreim  11250  absmul  11251  mul0inf  11423  mulcn2  11494  climmul  11509  isermulc2  11522  fsummulc2  11630  prodf  11720  clim2prod  11721  clim2divap  11722  prod3fmul  11723  prodf1  11724  prodfap0  11727  prodfrecap  11728  prodrbdclem  11753  fproddccvg  11754  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  fprodntrivap  11766  prodsnf  11774  fprodcl  11789  fprodclf  11817  efexp  11864  sinf  11886  cosf  11887  tanval2ap  11895  tanval3ap  11896  resinval  11897  recosval  11898  efi4p  11899  resin4p  11900  recos4p  11901  resincl  11902  recoscl  11903  sinneg  11908  cosneg  11909  efival  11914  efmival  11915  efeul  11916  sinadd  11918  cosadd  11919  sinsub  11922  cossub  11923  subsin  11925  sinmul  11926  cosmul  11927  addcos  11928  subcos  11929  cos2tsin  11933  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  absef  11952  absefib  11953  efieq1re  11954  demoivre  11955  demoivreALT  11956  odd2np1lem  12054  odd2np1  12055  opoe  12077  omoe  12078  opeo  12079  omeo  12080  modgcd  12183  qredeq  12289  modprm0  12448  pythagtriplem1  12459  pythagtriplem12  12469  pythagtriplem14  12471  gzmulcl  12572  4sqlem11  12595  4sqlem17  12601  cncrng  14201  cnfldmulg  14208  mpomulcn  14886  mulc1cncf  14909  mulcncflem  14927  dvmulxxbr  15022  dvmulxx  15024  dvimulf  15026  plymullem1  15068  plymulcl  15075  plysubcl  15076  efper  15127  sinperlem  15128  sin2kpi  15131  cos2kpi  15132  efimpi  15139  sincosq1eq  15159  abssinper  15166  sinkpi  15167  coskpi  15168  binom4  15299  fsumdvdsmul  15311  lgsdilem2  15361  lgsne0  15363  lgsquadlem1  15402  2sqlem2  15440