Theorem mulcl 7978

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2160  (class class class)co 5904  ℂcc 7849   · cmul 7856

This theorem was proved from axioms:  ax-mulcl 7949

This theorem is referenced by:  mpomulf  7988  0cn  7990  mulrid  7995  mulcli  8003  mulcld  8019  mul31  8129  mul4  8130  muladd11r  8154  cnegexlem2  8174  cnegex  8176  muladd  8382  subdi  8383  mul02  8385  submul2  8397  mulsub  8399  recextlem1  8649  recexap  8651  muleqadd  8666  divassap  8688  divmulassap  8693  divmuldivap  8710  divmuleqap  8715  divadddivap  8725  conjmulap  8727  cju  8959  zneo  9395  exp3vallem  10567  exp3val  10568  exp1  10572  expp1  10573  expcl  10584  expclzaplem  10590  mulexp  10605  sqcl  10627  subsq  10673  subsq2  10674  binom2sub  10680  mulbinom2  10683  binom3  10684  zesq  10685  bernneq  10687  bernneq2  10688  mulsubdivbinom2ap  10738  facnn  10754  fac0  10755  fac1  10756  facp1  10757  bcval5  10790  bcn2  10791  reim  10908  imcl  10910  crre  10913  crim  10914  remim  10916  mulreap  10920  cjreb  10922  recj  10923  reneg  10924  readd  10925  remullem  10927  remul2  10929  imcj  10931  imneg  10932  imadd  10933  immul2  10936  cjadd  10940  ipcnval  10942  cjmulrcl  10943  cjneg  10946  imval2  10950  cjreim  10959  rennim  11058  sqabsadd  11111  sqabssub  11112  absreimsq  11123  absreim  11124  absmul  11125  mul0inf  11296  mulcn2  11367  climmul  11382  isermulc2  11395  fsummulc2  11503  prodf  11593  clim2prod  11594  clim2divap  11595  prod3fmul  11596  prodf1  11597  prodfap0  11600  prodfrecap  11601  prodrbdclem  11626  fproddccvg  11627  prodmodclem3  11630  prodmodclem2a  11631  zproddc  11634  fprodseq  11638  fprodntrivap  11639  prodsnf  11647  fprodcl  11662  fprodclf  11690  efexp  11737  sinf  11759  cosf  11760  tanval2ap  11768  tanval3ap  11769  resinval  11770  recosval  11771  efi4p  11772  resin4p  11773  recos4p  11774  resincl  11775  recoscl  11776  sinneg  11781  cosneg  11782  efival  11787  efmival  11788  efeul  11789  sinadd  11791  cosadd  11792  sinsub  11795  cossub  11796  subsin  11798  sinmul  11799  cosmul  11800  addcos  11801  subcos  11802  cos2tsin  11806  ef01bndlem  11811  sin01bnd  11812  cos01bnd  11813  absef  11824  absefib  11825  efieq1re  11826  demoivre  11827  demoivreALT  11828  odd2np1lem  11924  odd2np1  11925  opoe  11947  omoe  11948  opeo  11949  omeo  11950  modgcd  12039  qredeq  12145  modprm0  12303  pythagtriplem1  12314  pythagtriplem12  12324  pythagtriplem14  12326  gzmulcl  12427  4sqlem11  12450  4sqlem17  12456  cncrng  13918  cnfldmulg  13925  mulc1cncf  14597  mulcncflem  14614  dvmulxxbr  14704  dvmulxx  14706  dvimulf  14708  efper  14766  sinperlem  14767  sin2kpi  14770  cos2kpi  14771  efimpi  14778  sincosq1eq  14798  abssinper  14805  sinkpi  14806  coskpi  14807  binom4  14935  lgsdilem2  14976  lgsne0  14978  2sqlem2  15001