Theorem mulcl 7665

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1461  (class class class)co 5726  ℂcc 7539   · cmul 7546

This theorem was proved from axioms:  ax-mulcl 7637

This theorem is referenced by:  0cn  7676  mulid1  7681  mulcli  7689  mulcld  7704  mul31  7810  mul4  7811  muladd11r  7835  cnegexlem2  7855  cnegex  7857  muladd  8059  subdi  8060  mul02  8062  submul2  8074  mulsub  8076  recextlem1  8319  recexap  8321  muleqadd  8336  divassap  8357  divmulassap  8362  divmuldivap  8379  divmuleqap  8384  divadddivap  8394  conjmulap  8396  cju  8623  zneo  9050  exp3vallem  10181  exp3val  10182  exp1  10186  expp1  10187  expcl  10198  expclzaplem  10204  mulexp  10219  sqcl  10241  subsq  10286  subsq2  10287  binom2sub  10292  mulbinom2  10295  binom3  10296  zesq  10297  bernneq  10299  bernneq2  10300  facnn  10360  fac0  10361  fac1  10362  facp1  10363  bcval5  10396  bcn2  10397  reim  10511  imcl  10513  crre  10516  crim  10517  remim  10519  mulreap  10523  cjreb  10525  recj  10526  reneg  10527  readd  10528  remullem  10530  remul2  10532  imcj  10534  imneg  10535  imadd  10536  immul2  10539  cjadd  10543  ipcnval  10545  cjmulrcl  10546  cjneg  10549  imval2  10553  cjreim  10562  rennim  10660  sqabsadd  10713  sqabssub  10714  absreimsq  10725  absreim  10726  absmul  10727  mul0inf  10898  mulcn2  10967  climmul  10982  isermulc2  10995  fsummulc2  11103  efexp  11233  sinf  11256  cosf  11257  tanval2ap  11265  tanval3ap  11266  resinval  11267  recosval  11268  efi4p  11269  resin4p  11270  recos4p  11271  resincl  11272  recoscl  11273  sinneg  11278  cosneg  11279  efival  11284  efmival  11285  efeul  11286  sinadd  11288  cosadd  11289  sinsub  11292  cossub  11293  subsin  11295  sinmul  11296  cosmul  11297  addcos  11298  subcos  11299  cos2tsin  11303  ef01bndlem  11308  sin01bnd  11309  cos01bnd  11310  absef  11320  absefib  11321  efieq1re  11322  demoivre  11323  demoivreALT  11324  odd2np1lem  11411  odd2np1  11412  opoe  11434  omoe  11435  opeo  11436  omeo  11437  modgcd  11521  qredeq  11617  mulc1cncf  12556  mulcncflem  12570