Theorem mulcl 7938

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  (class class class)co 5875  ℂcc 7809   · cmul 7816

This theorem was proved from axioms:  ax-mulcl 7909

This theorem is referenced by:  0cn  7949  mulrid  7954  mulcli  7962  mulcld  7978  mul31  8088  mul4  8089  muladd11r  8113  cnegexlem2  8133  cnegex  8135  muladd  8341  subdi  8342  mul02  8344  submul2  8356  mulsub  8358  recextlem1  8608  recexap  8610  muleqadd  8625  divassap  8647  divmulassap  8652  divmuldivap  8669  divmuleqap  8674  divadddivap  8684  conjmulap  8686  cju  8918  zneo  9354  exp3vallem  10521  exp3val  10522  exp1  10526  expp1  10527  expcl  10538  expclzaplem  10544  mulexp  10559  sqcl  10581  subsq  10627  subsq2  10628  binom2sub  10634  mulbinom2  10637  binom3  10638  zesq  10639  bernneq  10641  bernneq2  10642  mulsubdivbinom2ap  10691  facnn  10707  fac0  10708  fac1  10709  facp1  10710  bcval5  10743  bcn2  10744  reim  10861  imcl  10863  crre  10866  crim  10867  remim  10869  mulreap  10873  cjreb  10875  recj  10876  reneg  10877  readd  10878  remullem  10880  remul2  10882  imcj  10884  imneg  10885  imadd  10886  immul2  10889  cjadd  10893  ipcnval  10895  cjmulrcl  10896  cjneg  10899  imval2  10903  cjreim  10912  rennim  11011  sqabsadd  11064  sqabssub  11065  absreimsq  11076  absreim  11077  absmul  11078  mul0inf  11249  mulcn2  11320  climmul  11335  isermulc2  11348  fsummulc2  11456  prodf  11546  clim2prod  11547  clim2divap  11548  prod3fmul  11549  prodf1  11550  prodfap0  11553  prodfrecap  11554  prodrbdclem  11579  fproddccvg  11580  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodntrivap  11592  prodsnf  11600  fprodcl  11615  fprodclf  11643  efexp  11690  sinf  11712  cosf  11713  tanval2ap  11721  tanval3ap  11722  resinval  11723  recosval  11724  efi4p  11725  resin4p  11726  recos4p  11727  resincl  11728  recoscl  11729  sinneg  11734  cosneg  11735  efival  11740  efmival  11741  efeul  11742  sinadd  11744  cosadd  11745  sinsub  11748  cossub  11749  subsin  11751  sinmul  11752  cosmul  11753  addcos  11754  subcos  11755  cos2tsin  11759  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  absef  11777  absefib  11778  efieq1re  11779  demoivre  11780  demoivreALT  11781  odd2np1lem  11877  odd2np1  11878  opoe  11900  omoe  11901  opeo  11902  omeo  11903  modgcd  11992  qredeq  12096  modprm0  12254  pythagtriplem1  12265  pythagtriplem12  12275  pythagtriplem14  12277  gzmulcl  12376  cncrng  13466  cnfldmulg  13473  mulc1cncf  14079  mulcncflem  14093  dvmulxxbr  14169  dvmulxx  14171  dvimulf  14173  efper  14231  sinperlem  14232  sin2kpi  14235  cos2kpi  14236  efimpi  14243  sincosq1eq  14263  abssinper  14270  sinkpi  14271  coskpi  14272  binom4  14400  lgsdilem2  14440  lgsne0  14442  2sqlem2  14465