Theorem mulcl 8082

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  (class class class)co 5962  ℂcc 7953   · cmul 7960

This theorem was proved from axioms:  ax-mulcl 8053

This theorem is referenced by:  mpomulf  8092  0cn  8094  mulrid  8099  mulcli  8107  mulcld  8123  mul31  8233  mul4  8234  muladd11r  8258  cnegexlem2  8278  cnegex  8280  muladd  8486  subdi  8487  mul02  8489  submul2  8501  mulsub  8503  recextlem1  8754  recexap  8756  muleqadd  8771  divassap  8793  divmulassap  8798  divmuldivap  8815  divmuleqap  8820  divadddivap  8830  conjmulap  8832  cju  9064  ofnegsub  9065  zneo  9504  exp3vallem  10717  exp3val  10718  exp1  10722  expp1  10723  expcl  10734  expclzaplem  10740  mulexp  10755  sqcl  10777  subsq  10823  subsq2  10824  binom2sub  10830  mulbinom2  10833  binom3  10834  zesq  10835  bernneq  10837  bernneq2  10838  mulsubdivbinom2ap  10888  facnn  10904  fac0  10905  fac1  10906  facp1  10907  bcval5  10940  bcn2  10941  reim  11248  imcl  11250  crre  11253  crim  11254  remim  11256  mulreap  11260  cjreb  11262  recj  11263  reneg  11264  readd  11265  remullem  11267  remul2  11269  imcj  11271  imneg  11272  imadd  11273  immul2  11276  cjadd  11280  ipcnval  11282  cjmulrcl  11283  cjneg  11286  imval2  11290  cjreim  11299  rennim  11398  sqabsadd  11451  sqabssub  11452  absreimsq  11463  absreim  11464  absmul  11465  mul0inf  11637  mulcn2  11708  climmul  11723  isermulc2  11736  fsummulc2  11844  prodf  11934  clim2prod  11935  clim2divap  11936  prod3fmul  11937  prodf1  11938  prodfap0  11941  prodfrecap  11942  prodrbdclem  11967  fproddccvg  11968  prodmodclem3  11971  prodmodclem2a  11972  zproddc  11975  fprodseq  11979  fprodntrivap  11980  prodsnf  11988  fprodcl  12003  fprodclf  12031  efexp  12078  sinf  12100  cosf  12101  tanval2ap  12109  tanval3ap  12110  resinval  12111  recosval  12112  efi4p  12113  resin4p  12114  recos4p  12115  resincl  12116  recoscl  12117  sinneg  12122  cosneg  12123  efival  12128  efmival  12129  efeul  12130  sinadd  12132  cosadd  12133  sinsub  12136  cossub  12137  subsin  12139  sinmul  12140  cosmul  12141  addcos  12142  subcos  12143  cos2tsin  12147  ef01bndlem  12152  sin01bnd  12153  cos01bnd  12154  absef  12166  absefib  12167  efieq1re  12168  demoivre  12169  demoivreALT  12170  odd2np1lem  12268  odd2np1  12269  opoe  12291  omoe  12292  opeo  12293  omeo  12294  modgcd  12397  qredeq  12503  modprm0  12662  pythagtriplem1  12673  pythagtriplem12  12683  pythagtriplem14  12685  gzmulcl  12786  4sqlem11  12809  4sqlem17  12815  cncrng  14416  cnfldmulg  14423  mpomulcn  15123  mulc1cncf  15146  mulcncflem  15164  dvmulxxbr  15259  dvmulxx  15261  dvimulf  15263  plymullem1  15305  plymulcl  15312  plysubcl  15313  efper  15364  sinperlem  15365  sin2kpi  15368  cos2kpi  15369  efimpi  15376  sincosq1eq  15396  abssinper  15403  sinkpi  15404  coskpi  15405  binom4  15536  fsumdvdsmul  15548  lgsdilem2  15598  lgsne0  15600  lgsquadlem1  15639  2sqlem2  15677