Theorem mulcl 8152

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023   · cmul 8030

This theorem was proved from axioms:  ax-mulcl 8123

This theorem is referenced by:  mpomulf  8162  0cn  8164  mulrid  8169  mulcli  8177  mulcld  8193  mul31  8303  mul4  8304  muladd11r  8328  cnegexlem2  8348  cnegex  8350  muladd  8556  subdi  8557  mul02  8559  submul2  8571  mulsub  8573  recextlem1  8824  recexap  8826  muleqadd  8841  divassap  8863  divmulassap  8868  divmuldivap  8885  divmuleqap  8890  divadddivap  8900  conjmulap  8902  cju  9134  ofnegsub  9135  zneo  9574  exp3vallem  10795  exp3val  10796  exp1  10800  expp1  10801  expcl  10812  expclzaplem  10818  mulexp  10833  sqcl  10855  subsq  10901  subsq2  10902  binom2sub  10908  mulbinom2  10911  binom3  10912  zesq  10913  bernneq  10915  bernneq2  10916  mulsubdivbinom2ap  10966  facnn  10982  fac0  10983  fac1  10984  facp1  10985  bcval5  11018  bcn2  11019  reim  11406  imcl  11408  crre  11411  crim  11412  remim  11414  mulreap  11418  cjreb  11420  recj  11421  reneg  11422  readd  11423  remullem  11425  remul2  11427  imcj  11429  imneg  11430  imadd  11431  immul2  11434  cjadd  11438  ipcnval  11440  cjmulrcl  11441  cjneg  11444  imval2  11448  cjreim  11457  rennim  11556  sqabsadd  11609  sqabssub  11610  absreimsq  11621  absreim  11622  absmul  11623  mul0inf  11795  mulcn2  11866  climmul  11881  isermulc2  11894  fsummulc2  12002  prodf  12092  clim2prod  12093  clim2divap  12094  prod3fmul  12095  prodf1  12096  prodfap0  12099  prodfrecap  12100  prodrbdclem  12125  fproddccvg  12126  prodmodclem3  12129  prodmodclem2a  12130  zproddc  12133  fprodseq  12137  fprodntrivap  12138  prodsnf  12146  fprodcl  12161  fprodclf  12189  efexp  12236  sinf  12258  cosf  12259  tanval2ap  12267  tanval3ap  12268  resinval  12269  recosval  12270  efi4p  12271  resin4p  12272  recos4p  12273  resincl  12274  recoscl  12275  sinneg  12280  cosneg  12281  efival  12286  efmival  12287  efeul  12288  sinadd  12290  cosadd  12291  sinsub  12294  cossub  12295  subsin  12297  sinmul  12298  cosmul  12299  addcos  12300  subcos  12301  cos2tsin  12305  ef01bndlem  12310  sin01bnd  12311  cos01bnd  12312  absef  12324  absefib  12325  efieq1re  12326  demoivre  12327  demoivreALT  12328  odd2np1lem  12426  odd2np1  12427  opoe  12449  omoe  12450  opeo  12451  omeo  12452  modgcd  12555  qredeq  12661  modprm0  12820  pythagtriplem1  12831  pythagtriplem12  12841  pythagtriplem14  12843  gzmulcl  12944  4sqlem11  12967  4sqlem17  12973  cncrng  14576  cnfldmulg  14583  mpomulcn  15283  mulc1cncf  15306  mulcncflem  15324  dvmulxxbr  15419  dvmulxx  15421  dvimulf  15423  plymullem1  15465  plymulcl  15472  plysubcl  15473  efper  15524  sinperlem  15525  sin2kpi  15528  cos2kpi  15529  efimpi  15536  sincosq1eq  15556  abssinper  15563  sinkpi  15564  coskpi  15565  binom4  15696  fsumdvdsmul  15708  lgsdilem2  15758  lgsne0  15760  lgsquadlem1  15799  2sqlem2  15837