Theorem mulcl 8253

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  (class class class)co 6049  ℂcc 8124   · cmul 8131

This theorem was proved from axioms:  ax-mulcl 8224

This theorem is referenced by:  mpomulf  8263  0cn  8265  mulrid  8270  mulcli  8278  mulcld  8293  mul31  8403  mul4  8404  muladd11r  8428  cnegexlem2  8448  cnegex  8450  muladd  8656  subdi  8657  mul02  8659  submul2  8671  mulsub  8673  recextlem1  8924  recexap  8926  muleqadd  8941  divassap  8963  divmulassap  8968  divmuldivap  8985  divmuleqap  8990  divadddivap  9000  conjmulap  9002  cju  9234  ofnegsub  9235  zneo  9678  exp3vallem  10901  exp3val  10902  exp1  10906  expp1  10907  expcl  10918  expclzaplem  10924  mulexp  10939  sqcl  10961  subsq  11007  subsq2  11008  binom2sub  11014  mulbinom2  11017  binom3  11018  zesq  11019  bernneq  11021  bernneq2  11022  mulsubdivbinom2ap  11072  facnn  11088  fac0  11089  fac1  11090  facp1  11091  bcval5  11124  bcn2  11125  reim  11533  imcl  11535  crre  11538  crim  11539  remim  11541  mulreap  11545  cjreb  11547  recj  11548  reneg  11549  readd  11550  remullem  11552  remul2  11554  imcj  11556  imneg  11557  imadd  11558  immul2  11561  cjadd  11565  ipcnval  11567  cjmulrcl  11568  cjneg  11571  imval2  11575  cjreim  11584  rennim  11683  sqabsadd  11736  sqabssub  11737  absreimsq  11748  absreim  11749  absmul  11750  mul0inf  11922  mulcn2  11993  climmul  12008  isermulc2  12021  fsummulc2  12130  prodf  12220  clim2prod  12221  clim2divap  12222  prod3fmul  12223  prodf1  12224  prodfap0  12227  prodfrecap  12228  prodrbdclem  12253  fproddccvg  12254  prodmodclem3  12257  prodmodclem2a  12258  zproddc  12261  fprodseq  12265  fprodntrivap  12266  prodsnf  12274  fprodcl  12289  fprodclf  12317  efexp  12364  sinf  12386  cosf  12387  tanval2ap  12395  tanval3ap  12396  resinval  12397  recosval  12398  efi4p  12399  resin4p  12400  recos4p  12401  resincl  12402  recoscl  12403  sinneg  12408  cosneg  12409  efival  12414  efmival  12415  efeul  12416  sinadd  12418  cosadd  12419  sinsub  12422  cossub  12423  subsin  12425  sinmul  12426  cosmul  12427  addcos  12428  subcos  12429  cos2tsin  12433  ef01bndlem  12438  sin01bnd  12439  cos01bnd  12440  absef  12452  absefib  12453  efieq1re  12454  demoivre  12455  demoivreALT  12456  odd2np1lem  12554  odd2np1  12555  opoe  12577  omoe  12578  opeo  12579  omeo  12580  modgcd  12683  qredeq  12789  modprm0  12948  pythagtriplem1  12959  pythagtriplem12  12969  pythagtriplem14  12971  gzmulcl  13072  4sqlem11  13095  4sqlem17  13101  cncrng  14709  cnfldmulg  14716  mpomulcn  15423  mulc1cncf  15446  mulcncflem  15464  dvmulxxbr  15559  dvmulxx  15561  dvimulf  15563  plymullem1  15605  plymulcl  15612  plysubcl  15613  efper  15664  sinperlem  15665  sin2kpi  15668  cos2kpi  15669  efimpi  15676  sincosq1eq  15696  abssinper  15703  sinkpi  15704  coskpi  15705  binom4  15836  fsumdvdsmul  15851  lgsdilem2  15901  lgsne0  15903  lgsquadlem1  15942  2sqlem2  15980