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  9758  exp3vallem  10998  exp3val  10999  exp1  11003  expp1  11004  expcl  11015  expclzaplem  11021  mulexp  11036  sqcl  11058  subsq  11104  subsq2  11105  binom2sub  11111  mulbinom2  11114  binom3  11115  zesq  11117  bernneq  11119  bernneq2  11120  mulsubdivbinom2ap  11171  facnn  11187  fac0  11188  fac1  11189  facp1  11190  bcval5  11223  bcn2  11224  reim  11639  imcl  11641  crre  11644  crim  11645  remim  11647  mulreap  11651  cjreb  11653  recj  11654  reneg  11655  readd  11656  remullem  11658  remul2  11660  imcj  11662  imneg  11663  imadd  11664  immul2  11667  cjadd  11671  ipcnval  11673  cjmulrcl  11674  cjneg  11677  imval2  11681  cjreim  11691  rennim  11790  sqabsadd  11843  sqabssub  11844  absreimsq  11855  absreim  11856  absmul  11857  mul0inf  12032  mulcn2  12103  climmul  12118  isermulc2  12131  fsummulc2  12240  prodf  12330  clim2prod  12331  clim2divap  12332  prod3fmul  12333  prodf1  12334  prodfap0  12337  prodfrecap  12338  prodrbdclem  12363  fproddccvg  12364  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  fprodntrivap  12376  prodsnf  12384  fprodcl  12399  fprodclf  12427  efexp  12474  sinf  12496  cosf  12497  tanval2ap  12505  tanval3ap  12506  resinval  12507  recosval  12508  efi4p  12509  resin4p  12510  recos4p  12511  resincl  12512  recoscl  12513  sinneg  12518  cosneg  12519  efival  12524  efmival  12525  efeul  12526  sinadd  12528  cosadd  12529  sinsub  12532  cossub  12533  subsin  12535  sinmul  12536  cosmul  12537  addcos  12538  subcos  12539  cos2tsin  12543  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  absef  12562  absefib  12563  efieq1re  12564  demoivre  12565  demoivreALT  12566  odd2np1lem  12664  odd2np1  12665  opoe  12687  omoe  12688  opeo  12689  omeo  12690  modgcd  12793  qredeq  12899  modprm0  13062  pythagtriplem1  13073  pythagtriplem12  13083  pythagtriplem14  13085  gzmulcl  13186  4sqlem11  13209  4sqlem17  13215  cncrng  15015  cnfldmulg  15022  mpomulcn  15825  mulc1cncf  15848  mulcncflem  15866  dvmulxxbr  15961  dvmulxx  15963  dvimulf  15965  plymullem1  16007  plymulcl  16014  plysubcl  16015  efper  16067  sinperlem  16068  sin2kpi  16071  cos2kpi  16072  efimpi  16079  sincosq1eq  16099  abssinper  16106  sinkpi  16107  coskpi  16108  sineq0re  16109  binom4  16252  prmorcht  16315  fsumdvdsmul  16318  ppiqub  16326  bposlem9  16352  lgsdilem2  16393  lgsne0  16395  lgsquadlem1  16434  2sqlem2  16472