Theorem mulcl 8307

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

Assertion

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

Proof of Theorem mulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  (class class class)co 6085  ℂcc 8178   · cmul 8185

This proof depends on axioms:  ax-mulcl 8278

This theorem is used by:  mpomulf  8317  0cn  8319  mulrid  8324  mulcli  8332  mulcld  8347  mul31  8459  mul4  8460  muladd11r  8484  cnegexlem2  8504  cnegex  8506  muladd  8713  subdi  8714  mul02  8716  submul2  8728  mulsub  8730  recextlem1  8982  recexap  8984  muleqadd  9001  divassap  9023  divmulassap  9028  divmuldivap  9045  divmuleqap  9050  divadddivap  9060  conjmulap  9062  cju  9294  ofnegsub  9295  zneo  9752  exp3vallem  10991  exp3val  10992  exp1  10996  expp1  10997  expcl  11008  expclzaplem  11014  mulexp  11029  sqcl  11051  subsq  11097  subsq2  11098  binom2sub  11104  mulbinom2  11107  binom3  11108  zesq  11110  bernneq  11112  bernneq2  11113  mulsubdivbinom2ap  11164  facnn  11180  fac0  11181  fac1  11182  facp1  11183  bcval5  11216  bcn2  11217  reim  11632  imcl  11634  crre  11637  crim  11638  remim  11640  mulreap  11644  cjreb  11646  recj  11647  reneg  11648  readd  11649  remullem  11651  remul2  11653  imcj  11655  imneg  11656  imadd  11657  immul2  11660  cjadd  11664  ipcnval  11666  cjmulrcl  11667  cjneg  11670  imval2  11674  cjreim  11684  rennim  11783  sqabsadd  11836  sqabssub  11837  absreimsq  11848  absreim  11849  absmul  11850  mul0inf  12025  mulcn2  12096  climmul  12111  isermulc2  12124  fsummulc2  12233  prodf  12323  clim2prod  12324  clim2divap  12325  prod3fmul  12326  prodf1  12327  prodfap0  12330  prodfrecap  12331  prodrbdclem  12356  fproddccvg  12357  prodmodclem3  12360  prodmodclem2a  12361  zproddc  12364  fprodseq  12368  fprodntrivap  12369  prodsnf  12377  fprodcl  12392  fprodclf  12420  efexp  12467  sinf  12489  cosf  12490  tanval2ap  12498  tanval3ap  12499  resinval  12500  recosval  12501  efi4p  12502  resin4p  12503  recos4p  12504  resincl  12505  recoscl  12506  sinneg  12511  cosneg  12512  efival  12517  efmival  12518  efeul  12519  sinadd  12521  cosadd  12522  sinsub  12525  cossub  12526  subsin  12528  sinmul  12529  cosmul  12530  addcos  12531  subcos  12532  cos2tsin  12536  ef01bndlem  12541  sin01bnd  12542  cos01bnd  12543  absef  12555  absefib  12556  efieq1re  12557  demoivre  12558  demoivreALT  12559  odd2np1lem  12657  odd2np1  12658  opoe  12680  omoe  12681  opeo  12682  omeo  12683  modgcd  12786  qredeq  12892  modprm0  13055  pythagtriplem1  13066  pythagtriplem12  13076  pythagtriplem14  13078  gzmulcl  13179  4sqlem11  13202  4sqlem17  13208  cncrng  14957  cnfldmulg  14964  mpomulcn  15719  mulc1cncf  15742  mulcncflem  15760  dvmulxxbr  15855  dvmulxx  15857  dvimulf  15859  plymullem1  15901  plymulcl  15908  plysubcl  15909  efper  15961  sinperlem  15962  sin2kpi  15965  cos2kpi  15966  efimpi  15973  sincosq1eq  15993  abssinper  16000  sinkpi  16001  coskpi  16002  binom4  16141  prmorcht  16204  fsumdvdsmul  16207  ppiqub  16215  lgsdilem2  16277  lgsne0  16279  lgsquadlem1  16318  2sqlem2  16356