Theorem mulcl 8137

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

Assertion

Ref	Expression
mulcl	|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Proof of Theorem mulcl

Step	Hyp	Ref	Expression
1		ax-mulcl 8108	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200  (class class class)co 6007   CCcc 8008   x. cmul 8015

This theorem was proved from axioms:  ax-mulcl 8108

This theorem is referenced by:  mpomulf  8147  0cn  8149  mulrid  8154  mulcli  8162  mulcld  8178  mul31  8288  mul4  8289  muladd11r  8313  cnegexlem2  8333  cnegex  8335  muladd  8541  subdi  8542  mul02  8544  submul2  8556  mulsub  8558  recextlem1  8809  recexap  8811  muleqadd  8826  divassap  8848  divmulassap  8853  divmuldivap  8870  divmuleqap  8875  divadddivap  8885  conjmulap  8887  cju  9119  ofnegsub  9120  zneo  9559  exp3vallem  10774  exp3val  10775  exp1  10779  expp1  10780  expcl  10791  expclzaplem  10797  mulexp  10812  sqcl  10834  subsq  10880  subsq2  10881  binom2sub  10887  mulbinom2  10890  binom3  10891  zesq  10892  bernneq  10894  bernneq2  10895  mulsubdivbinom2ap  10945  facnn  10961  fac0  10962  fac1  10963  facp1  10964  bcval5  10997  bcn2  10998  reim  11378  imcl  11380  crre  11383  crim  11384  remim  11386  mulreap  11390  cjreb  11392  recj  11393  reneg  11394  readd  11395  remullem  11397  remul2  11399  imcj  11401  imneg  11402  imadd  11403  immul2  11406  cjadd  11410  ipcnval  11412  cjmulrcl  11413  cjneg  11416  imval2  11420  cjreim  11429  rennim  11528  sqabsadd  11581  sqabssub  11582  absreimsq  11593  absreim  11594  absmul  11595  mul0inf  11767  mulcn2  11838  climmul  11853  isermulc2  11866  fsummulc2  11974  prodf  12064  clim2prod  12065  clim2divap  12066  prod3fmul  12067  prodf1  12068  prodfap0  12071  prodfrecap  12072  prodrbdclem  12097  fproddccvg  12098  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  fprodntrivap  12110  prodsnf  12118  fprodcl  12133  fprodclf  12161  efexp  12208  sinf  12230  cosf  12231  tanval2ap  12239  tanval3ap  12240  resinval  12241  recosval  12242  efi4p  12243  resin4p  12244  recos4p  12245  resincl  12246  recoscl  12247  sinneg  12252  cosneg  12253  efival  12258  efmival  12259  efeul  12260  sinadd  12262  cosadd  12263  sinsub  12266  cossub  12267  subsin  12269  sinmul  12270  cosmul  12271  addcos  12272  subcos  12273  cos2tsin  12277  ef01bndlem  12282  sin01bnd  12283  cos01bnd  12284  absef  12296  absefib  12297  efieq1re  12298  demoivre  12299  demoivreALT  12300  odd2np1lem  12398  odd2np1  12399  opoe  12421  omoe  12422  opeo  12423  omeo  12424  modgcd  12527  qredeq  12633  modprm0  12792  pythagtriplem1  12803  pythagtriplem12  12813  pythagtriplem14  12815  gzmulcl  12916  4sqlem11  12939  4sqlem17  12945  cncrng  14548  cnfldmulg  14555  mpomulcn  15255  mulc1cncf  15278  mulcncflem  15296  dvmulxxbr  15391  dvmulxx  15393  dvimulf  15395  plymullem1  15437  plymulcl  15444  plysubcl  15445  efper  15496  sinperlem  15497  sin2kpi  15500  cos2kpi  15501  efimpi  15508  sincosq1eq  15528  abssinper  15535  sinkpi  15536  coskpi  15537  binom4  15668  fsumdvdsmul  15680  lgsdilem2  15730  lgsne0  15732  lgsquadlem1  15771  2sqlem2  15809