Theorem mulcl 7901

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141  (class class class)co 5853  ℂcc 7772   · cmul 7779

This theorem was proved from axioms:  ax-mulcl 7872

This theorem is referenced by:  0cn  7912  mulid1  7917  mulcli  7925  mulcld  7940  mul31  8050  mul4  8051  muladd11r  8075  cnegexlem2  8095  cnegex  8097  muladd  8303  subdi  8304  mul02  8306  submul2  8318  mulsub  8320  recextlem1  8569  recexap  8571  muleqadd  8586  divassap  8607  divmulassap  8612  divmuldivap  8629  divmuleqap  8634  divadddivap  8644  conjmulap  8646  cju  8877  zneo  9313  exp3vallem  10477  exp3val  10478  exp1  10482  expp1  10483  expcl  10494  expclzaplem  10500  mulexp  10515  sqcl  10537  subsq  10582  subsq2  10583  binom2sub  10589  mulbinom2  10592  binom3  10593  zesq  10594  bernneq  10596  bernneq2  10597  facnn  10661  fac0  10662  fac1  10663  facp1  10664  bcval5  10697  bcn2  10698  reim  10816  imcl  10818  crre  10821  crim  10822  remim  10824  mulreap  10828  cjreb  10830  recj  10831  reneg  10832  readd  10833  remullem  10835  remul2  10837  imcj  10839  imneg  10840  imadd  10841  immul2  10844  cjadd  10848  ipcnval  10850  cjmulrcl  10851  cjneg  10854  imval2  10858  cjreim  10867  rennim  10966  sqabsadd  11019  sqabssub  11020  absreimsq  11031  absreim  11032  absmul  11033  mul0inf  11204  mulcn2  11275  climmul  11290  isermulc2  11303  fsummulc2  11411  prodf  11501  clim2prod  11502  clim2divap  11503  prod3fmul  11504  prodf1  11505  prodfap0  11508  prodfrecap  11509  prodrbdclem  11534  fproddccvg  11535  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodntrivap  11547  prodsnf  11555  fprodcl  11570  fprodclf  11598  efexp  11645  sinf  11667  cosf  11668  tanval2ap  11676  tanval3ap  11677  resinval  11678  recosval  11679  efi4p  11680  resin4p  11681  recos4p  11682  resincl  11683  recoscl  11684  sinneg  11689  cosneg  11690  efival  11695  efmival  11696  efeul  11697  sinadd  11699  cosadd  11700  sinsub  11703  cossub  11704  subsin  11706  sinmul  11707  cosmul  11708  addcos  11709  subcos  11710  cos2tsin  11714  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  absef  11732  absefib  11733  efieq1re  11734  demoivre  11735  demoivreALT  11736  odd2np1lem  11831  odd2np1  11832  opoe  11854  omoe  11855  opeo  11856  omeo  11857  modgcd  11946  qredeq  12050  modprm0  12208  pythagtriplem1  12219  pythagtriplem12  12229  pythagtriplem14  12231  gzmulcl  12330  mulc1cncf  13370  mulcncflem  13384  dvmulxxbr  13460  dvmulxx  13462  dvimulf  13464  efper  13522  sinperlem  13523  sin2kpi  13526  cos2kpi  13527  efimpi  13534  sincosq1eq  13554  abssinper  13561  sinkpi  13562  coskpi  13563  binom4  13691  lgsdilem2  13731  lgsne0  13733  2sqlem2  13745