Theorem mulcl 8134

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005   · cmul 8012

This theorem was proved from axioms:  ax-mulcl 8105

This theorem is referenced by:  mpomulf  8144  0cn  8146  mulrid  8151  mulcli  8159  mulcld  8175  mul31  8285  mul4  8286  muladd11r  8310  cnegexlem2  8330  cnegex  8332  muladd  8538  subdi  8539  mul02  8541  submul2  8553  mulsub  8555  recextlem1  8806  recexap  8808  muleqadd  8823  divassap  8845  divmulassap  8850  divmuldivap  8867  divmuleqap  8872  divadddivap  8882  conjmulap  8884  cju  9116  ofnegsub  9117  zneo  9556  exp3vallem  10770  exp3val  10771  exp1  10775  expp1  10776  expcl  10787  expclzaplem  10793  mulexp  10808  sqcl  10830  subsq  10876  subsq2  10877  binom2sub  10883  mulbinom2  10886  binom3  10887  zesq  10888  bernneq  10890  bernneq2  10891  mulsubdivbinom2ap  10941  facnn  10957  fac0  10958  fac1  10959  facp1  10960  bcval5  10993  bcn2  10994  reim  11371  imcl  11373  crre  11376  crim  11377  remim  11379  mulreap  11383  cjreb  11385  recj  11386  reneg  11387  readd  11388  remullem  11390  remul2  11392  imcj  11394  imneg  11395  imadd  11396  immul2  11399  cjadd  11403  ipcnval  11405  cjmulrcl  11406  cjneg  11409  imval2  11413  cjreim  11422  rennim  11521  sqabsadd  11574  sqabssub  11575  absreimsq  11586  absreim  11587  absmul  11588  mul0inf  11760  mulcn2  11831  climmul  11846  isermulc2  11859  fsummulc2  11967  prodf  12057  clim2prod  12058  clim2divap  12059  prod3fmul  12060  prodf1  12061  prodfap0  12064  prodfrecap  12065  prodrbdclem  12090  fproddccvg  12091  prodmodclem3  12094  prodmodclem2a  12095  zproddc  12098  fprodseq  12102  fprodntrivap  12103  prodsnf  12111  fprodcl  12126  fprodclf  12154  efexp  12201  sinf  12223  cosf  12224  tanval2ap  12232  tanval3ap  12233  resinval  12234  recosval  12235  efi4p  12236  resin4p  12237  recos4p  12238  resincl  12239  recoscl  12240  sinneg  12245  cosneg  12246  efival  12251  efmival  12252  efeul  12253  sinadd  12255  cosadd  12256  sinsub  12259  cossub  12260  subsin  12262  sinmul  12263  cosmul  12264  addcos  12265  subcos  12266  cos2tsin  12270  ef01bndlem  12275  sin01bnd  12276  cos01bnd  12277  absef  12289  absefib  12290  efieq1re  12291  demoivre  12292  demoivreALT  12293  odd2np1lem  12391  odd2np1  12392  opoe  12414  omoe  12415  opeo  12416  omeo  12417  modgcd  12520  qredeq  12626  modprm0  12785  pythagtriplem1  12796  pythagtriplem12  12806  pythagtriplem14  12808  gzmulcl  12909  4sqlem11  12932  4sqlem17  12938  cncrng  14541  cnfldmulg  14548  mpomulcn  15248  mulc1cncf  15271  mulcncflem  15289  dvmulxxbr  15384  dvmulxx  15386  dvimulf  15388  plymullem1  15430  plymulcl  15437  plysubcl  15438  efper  15489  sinperlem  15490  sin2kpi  15493  cos2kpi  15494  efimpi  15501  sincosq1eq  15521  abssinper  15528  sinkpi  15529  coskpi  15530  binom4  15661  fsumdvdsmul  15673  lgsdilem2  15723  lgsne0  15725  lgsquadlem1  15764  2sqlem2  15802