Theorem mulcl 8142

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013   · cmul 8020

This theorem was proved from axioms:  ax-mulcl 8113

This theorem is referenced by:  mpomulf  8152  0cn  8154  mulrid  8159  mulcli  8167  mulcld  8183  mul31  8293  mul4  8294  muladd11r  8318  cnegexlem2  8338  cnegex  8340  muladd  8546  subdi  8547  mul02  8549  submul2  8561  mulsub  8563  recextlem1  8814  recexap  8816  muleqadd  8831  divassap  8853  divmulassap  8858  divmuldivap  8875  divmuleqap  8880  divadddivap  8890  conjmulap  8892  cju  9124  ofnegsub  9125  zneo  9564  exp3vallem  10779  exp3val  10780  exp1  10784  expp1  10785  expcl  10796  expclzaplem  10802  mulexp  10817  sqcl  10839  subsq  10885  subsq2  10886  binom2sub  10892  mulbinom2  10895  binom3  10896  zesq  10897  bernneq  10899  bernneq2  10900  mulsubdivbinom2ap  10950  facnn  10966  fac0  10967  fac1  10968  facp1  10969  bcval5  11002  bcn2  11003  reim  11384  imcl  11386  crre  11389  crim  11390  remim  11392  mulreap  11396  cjreb  11398  recj  11399  reneg  11400  readd  11401  remullem  11403  remul2  11405  imcj  11407  imneg  11408  imadd  11409  immul2  11412  cjadd  11416  ipcnval  11418  cjmulrcl  11419  cjneg  11422  imval2  11426  cjreim  11435  rennim  11534  sqabsadd  11587  sqabssub  11588  absreimsq  11599  absreim  11600  absmul  11601  mul0inf  11773  mulcn2  11844  climmul  11859  isermulc2  11872  fsummulc2  11980  prodf  12070  clim2prod  12071  clim2divap  12072  prod3fmul  12073  prodf1  12074  prodfap0  12077  prodfrecap  12078  prodrbdclem  12103  fproddccvg  12104  prodmodclem3  12107  prodmodclem2a  12108  zproddc  12111  fprodseq  12115  fprodntrivap  12116  prodsnf  12124  fprodcl  12139  fprodclf  12167  efexp  12214  sinf  12236  cosf  12237  tanval2ap  12245  tanval3ap  12246  resinval  12247  recosval  12248  efi4p  12249  resin4p  12250  recos4p  12251  resincl  12252  recoscl  12253  sinneg  12258  cosneg  12259  efival  12264  efmival  12265  efeul  12266  sinadd  12268  cosadd  12269  sinsub  12272  cossub  12273  subsin  12275  sinmul  12276  cosmul  12277  addcos  12278  subcos  12279  cos2tsin  12283  ef01bndlem  12288  sin01bnd  12289  cos01bnd  12290  absef  12302  absefib  12303  efieq1re  12304  demoivre  12305  demoivreALT  12306  odd2np1lem  12404  odd2np1  12405  opoe  12427  omoe  12428  opeo  12429  omeo  12430  modgcd  12533  qredeq  12639  modprm0  12798  pythagtriplem1  12809  pythagtriplem12  12819  pythagtriplem14  12821  gzmulcl  12922  4sqlem11  12945  4sqlem17  12951  cncrng  14554  cnfldmulg  14561  mpomulcn  15261  mulc1cncf  15284  mulcncflem  15302  dvmulxxbr  15397  dvmulxx  15399  dvimulf  15401  plymullem1  15443  plymulcl  15450  plysubcl  15451  efper  15502  sinperlem  15503  sin2kpi  15506  cos2kpi  15507  efimpi  15514  sincosq1eq  15534  abssinper  15541  sinkpi  15542  coskpi  15543  binom4  15674  fsumdvdsmul  15686  lgsdilem2  15736  lgsne0  15738  lgsquadlem1  15777  2sqlem2  15815