Theorem mulcl 8313

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

Assertion

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

Proof of Theorem mulcl

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

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

This proof depends on axioms:  ax-mulcl 8284

This theorem is used by:  mpomulf  8323  0cn  8325  mulrid  8330  mulcli  8338  mulcld  8353  mul31  8465  mul4  8466  muladd11r  8490  cnegexlem2  8510  cnegex  8512  muladd  8719  subdi  8720  mul02  8722  submul2  8734  mulsub  8736  recextlem1  8988  recexap  8990  muleqadd  9007  divassap  9029  divmulassap  9034  divmuldivap  9051  divmuleqap  9056  divadddivap  9066  conjmulap  9068  cju  9300  ofnegsub  9302  zneo  9759  exp3vallem  10999  exp3val  11000  exp1  11004  expp1  11005  expcl  11016  expclzaplem  11022  mulexp  11037  sqcl  11059  subsq  11105  subsq2  11106  binom2sub  11112  mulbinom2  11115  binom3  11116  zesq  11118  bernneq  11120  bernneq2  11121  mulsubdivbinom2ap  11172  facnn  11188  fac0  11189  fac1  11190  facp1  11191  bcval5  11224  bcn2  11225  reim  11640  imcl  11642  crre  11645  crim  11646  remim  11648  mulreap  11652  cjreb  11654  recj  11655  reneg  11656  readd  11657  remullem  11659  remul2  11661  imcj  11663  imneg  11664  imadd  11665  immul2  11668  cjadd  11672  ipcnval  11674  cjmulrcl  11675  cjneg  11678  imval2  11682  cjreim  11692  rennim  11791  sqabsadd  11844  sqabssub  11845  absreimsq  11856  absreim  11857  absmul  11858  mul0inf  12033  mulcn2  12104  climmul  12119  isermulc2  12132  fsummulc2  12241  prodf  12331  clim2prod  12332  clim2divap  12333  prod3fmul  12334  prodf1  12335  prodfap0  12338  prodfrecap  12339  prodrbdclem  12364  fproddccvg  12365  prodmodclem3  12368  prodmodclem2a  12369  zproddc  12372  fprodseq  12376  fprodntrivap  12377  prodsnf  12385  fprodcl  12400  fprodclf  12428  efexp  12475  sinf  12497  cosf  12498  tanval2ap  12506  tanval3ap  12507  resinval  12508  recosval  12509  efi4p  12510  resin4p  12511  recos4p  12512  resincl  12513  recoscl  12514  sinneg  12519  cosneg  12520  efival  12525  efmival  12526  efeul  12527  sinadd  12529  cosadd  12530  sinsub  12533  cossub  12534  subsin  12536  sinmul  12537  cosmul  12538  addcos  12539  subcos  12540  cos2tsin  12544  ef01bndlem  12549  sin01bnd  12550  cos01bnd  12551  absef  12563  absefib  12564  efieq1re  12565  demoivre  12566  demoivreALT  12567  odd2np1lem  12665  odd2np1  12666  opoe  12688  omoe  12689  opeo  12690  omeo  12691  modgcd  12794  qredeq  12900  modprm0  13063  pythagtriplem1  13074  pythagtriplem12  13084  pythagtriplem14  13086  gzmulcl  13187  4sqlem11  13210  4sqlem17  13216  cncrng  15016  cnfldmulg  15023  mpomulcn  15804  mulc1cncf  15827  mulcncflem  15845  dvmulxxbr  15940  dvmulxx  15942  dvimulf  15944  plymullem1  15986  plymulcl  15993  plysubcl  15994  efper  16046  sinperlem  16047  sin2kpi  16050  cos2kpi  16051  efimpi  16058  sincosq1eq  16078  abssinper  16085  sinkpi  16086  coskpi  16087  sineq0re  16088  binom4  16231  prmorcht  16294  fsumdvdsmul  16297  ppiqub  16305  bposlem9  16331  lgsdilem2  16372  lgsne0  16374  lgsquadlem1  16413  2sqlem2  16451