Theorem mulcl 8065

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

Assertion

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

Proof of Theorem mulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  (class class class)co 5954  ℂcc 7936   · cmul 7943

This theorem was proved from axioms:  ax-mulcl 8036

This theorem is referenced by:  mpomulf  8075  0cn  8077  mulrid  8082  mulcli  8090  mulcld  8106  mul31  8216  mul4  8217  muladd11r  8241  cnegexlem2  8261  cnegex  8263  muladd  8469  subdi  8470  mul02  8472  submul2  8484  mulsub  8486  recextlem1  8737  recexap  8739  muleqadd  8754  divassap  8776  divmulassap  8781  divmuldivap  8798  divmuleqap  8803  divadddivap  8813  conjmulap  8815  cju  9047  ofnegsub  9048  zneo  9487  exp3vallem  10698  exp3val  10699  exp1  10703  expp1  10704  expcl  10715  expclzaplem  10721  mulexp  10736  sqcl  10758  subsq  10804  subsq2  10805  binom2sub  10811  mulbinom2  10814  binom3  10815  zesq  10816  bernneq  10818  bernneq2  10819  mulsubdivbinom2ap  10869  facnn  10885  fac0  10886  fac1  10887  facp1  10888  bcval5  10921  bcn2  10922  reim  11213  imcl  11215  crre  11218  crim  11219  remim  11221  mulreap  11225  cjreb  11227  recj  11228  reneg  11229  readd  11230  remullem  11232  remul2  11234  imcj  11236  imneg  11237  imadd  11238  immul2  11241  cjadd  11245  ipcnval  11247  cjmulrcl  11248  cjneg  11251  imval2  11255  cjreim  11264  rennim  11363  sqabsadd  11416  sqabssub  11417  absreimsq  11428  absreim  11429  absmul  11430  mul0inf  11602  mulcn2  11673  climmul  11688  isermulc2  11701  fsummulc2  11809  prodf  11899  clim2prod  11900  clim2divap  11901  prod3fmul  11902  prodf1  11903  prodfap0  11906  prodfrecap  11907  prodrbdclem  11932  fproddccvg  11933  prodmodclem3  11936  prodmodclem2a  11937  zproddc  11940  fprodseq  11944  fprodntrivap  11945  prodsnf  11953  fprodcl  11968  fprodclf  11996  efexp  12043  sinf  12065  cosf  12066  tanval2ap  12074  tanval3ap  12075  resinval  12076  recosval  12077  efi4p  12078  resin4p  12079  recos4p  12080  resincl  12081  recoscl  12082  sinneg  12087  cosneg  12088  efival  12093  efmival  12094  efeul  12095  sinadd  12097  cosadd  12098  sinsub  12101  cossub  12102  subsin  12104  sinmul  12105  cosmul  12106  addcos  12107  subcos  12108  cos2tsin  12112  ef01bndlem  12117  sin01bnd  12118  cos01bnd  12119  absef  12131  absefib  12132  efieq1re  12133  demoivre  12134  demoivreALT  12135  odd2np1lem  12233  odd2np1  12234  opoe  12256  omoe  12257  opeo  12258  omeo  12259  modgcd  12362  qredeq  12468  modprm0  12627  pythagtriplem1  12638  pythagtriplem12  12648  pythagtriplem14  12650  gzmulcl  12751  4sqlem11  12774  4sqlem17  12780  cncrng  14381  cnfldmulg  14388  mpomulcn  15088  mulc1cncf  15111  mulcncflem  15129  dvmulxxbr  15224  dvmulxx  15226  dvimulf  15228  plymullem1  15270  plymulcl  15277  plysubcl  15278  efper  15329  sinperlem  15330  sin2kpi  15333  cos2kpi  15334  efimpi  15341  sincosq1eq  15361  abssinper  15368  sinkpi  15369  coskpi  15370  binom4  15501  fsumdvdsmul  15513  lgsdilem2  15563  lgsne0  15565  lgsquadlem1  15604  2sqlem2  15642