Theorem mulcl 8300

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   · cmul 8178

This theorem was proved from axioms:  ax-mulcl 8271

This theorem is referenced by:  mpomulf  8310  0cn  8312  mulrid  8317  mulcli  8325  mulcld  8340  mul31  8451  mul4  8452  muladd11r  8476  cnegexlem2  8496  cnegex  8498  muladd  8705  subdi  8706  mul02  8708  submul2  8720  mulsub  8722  recextlem1  8973  recexap  8975  muleqadd  8992  divassap  9014  divmulassap  9019  divmuldivap  9036  divmuleqap  9041  divadddivap  9051  conjmulap  9053  cju  9285  ofnegsub  9286  zneo  9730  exp3vallem  10960  exp3val  10961  exp1  10965  expp1  10966  expcl  10977  expclzaplem  10983  mulexp  10998  sqcl  11020  subsq  11066  subsq2  11067  binom2sub  11073  mulbinom2  11076  binom3  11077  zesq  11079  bernneq  11081  bernneq2  11082  mulsubdivbinom2ap  11132  facnn  11148  fac0  11149  fac1  11150  facp1  11151  bcval5  11184  bcn2  11185  reim  11600  imcl  11602  crre  11605  crim  11606  remim  11608  mulreap  11612  cjreb  11614  recj  11615  reneg  11616  readd  11617  remullem  11619  remul2  11621  imcj  11623  imneg  11624  imadd  11625  immul2  11628  cjadd  11632  ipcnval  11634  cjmulrcl  11635  cjneg  11638  imval2  11642  cjreim  11652  rennim  11751  sqabsadd  11804  sqabssub  11805  absreimsq  11816  absreim  11817  absmul  11818  mul0inf  11990  mulcn2  12061  climmul  12076  isermulc2  12089  fsummulc2  12198  prodf  12288  clim2prod  12289  clim2divap  12290  prod3fmul  12291  prodf1  12292  prodfap0  12295  prodfrecap  12296  prodrbdclem  12321  fproddccvg  12322  prodmodclem3  12325  prodmodclem2a  12326  zproddc  12329  fprodseq  12333  fprodntrivap  12334  prodsnf  12342  fprodcl  12357  fprodclf  12385  efexp  12432  sinf  12454  cosf  12455  tanval2ap  12463  tanval3ap  12464  resinval  12465  recosval  12466  efi4p  12467  resin4p  12468  recos4p  12469  resincl  12470  recoscl  12471  sinneg  12476  cosneg  12477  efival  12482  efmival  12483  efeul  12484  sinadd  12486  cosadd  12487  sinsub  12490  cossub  12491  subsin  12493  sinmul  12494  cosmul  12495  addcos  12496  subcos  12497  cos2tsin  12501  ef01bndlem  12506  sin01bnd  12507  cos01bnd  12508  absef  12520  absefib  12521  efieq1re  12522  demoivre  12523  demoivreALT  12524  odd2np1lem  12622  odd2np1  12623  opoe  12645  omoe  12646  opeo  12647  omeo  12648  modgcd  12751  qredeq  12857  modprm0  13016  pythagtriplem1  13027  pythagtriplem12  13037  pythagtriplem14  13039  gzmulcl  13140  4sqlem11  13163  4sqlem17  13169  cncrng  14889  cnfldmulg  14896  mpomulcn  15650  mulc1cncf  15673  mulcncflem  15691  dvmulxxbr  15786  dvmulxx  15788  dvimulf  15790  plymullem1  15832  plymulcl  15839  plysubcl  15840  efper  15891  sinperlem  15892  sin2kpi  15895  cos2kpi  15896  efimpi  15903  sincosq1eq  15923  abssinper  15930  sinkpi  15931  coskpi  15932  binom4  16064  fsumdvdsmul  16088  lgsdilem2  16138  lgsne0  16140  lgsquadlem1  16179  2sqlem2  16217