Theorem mulcl 8158

Description: Alias for ax-mulcl 8129, for naming consistency with mulcli 8183. (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 8129	1 |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202  (class class class)co 6017   CCcc 8029   x. cmul 8036

This theorem was proved from axioms:  ax-mulcl 8129

This theorem is referenced by:  mpomulf  8168  0cn  8170  mulrid  8175  mulcli  8183  mulcld  8199  mul31  8309  mul4  8310  muladd11r  8334  cnegexlem2  8354  cnegex  8356  muladd  8562  subdi  8563  mul02  8565  submul2  8577  mulsub  8579  recextlem1  8830  recexap  8832  muleqadd  8847  divassap  8869  divmulassap  8874  divmuldivap  8891  divmuleqap  8896  divadddivap  8906  conjmulap  8908  cju  9140  ofnegsub  9141  zneo  9580  exp3vallem  10801  exp3val  10802  exp1  10806  expp1  10807  expcl  10818  expclzaplem  10824  mulexp  10839  sqcl  10861  subsq  10907  subsq2  10908  binom2sub  10914  mulbinom2  10917  binom3  10918  zesq  10919  bernneq  10921  bernneq2  10922  mulsubdivbinom2ap  10972  facnn  10988  fac0  10989  fac1  10990  facp1  10991  bcval5  11024  bcn2  11025  reim  11412  imcl  11414  crre  11417  crim  11418  remim  11420  mulreap  11424  cjreb  11426  recj  11427  reneg  11428  readd  11429  remullem  11431  remul2  11433  imcj  11435  imneg  11436  imadd  11437  immul2  11440  cjadd  11444  ipcnval  11446  cjmulrcl  11447  cjneg  11450  imval2  11454  cjreim  11463  rennim  11562  sqabsadd  11615  sqabssub  11616  absreimsq  11627  absreim  11628  absmul  11629  mul0inf  11801  mulcn2  11872  climmul  11887  isermulc2  11900  fsummulc2  12008  prodf  12098  clim2prod  12099  clim2divap  12100  prod3fmul  12101  prodf1  12102  prodfap0  12105  prodfrecap  12106  prodrbdclem  12131  fproddccvg  12132  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  fprodntrivap  12144  prodsnf  12152  fprodcl  12167  fprodclf  12195  efexp  12242  sinf  12264  cosf  12265  tanval2ap  12273  tanval3ap  12274  resinval  12275  recosval  12276  efi4p  12277  resin4p  12278  recos4p  12279  resincl  12280  recoscl  12281  sinneg  12286  cosneg  12287  efival  12292  efmival  12293  efeul  12294  sinadd  12296  cosadd  12297  sinsub  12300  cossub  12301  subsin  12303  sinmul  12304  cosmul  12305  addcos  12306  subcos  12307  cos2tsin  12311  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  absef  12330  absefib  12331  efieq1re  12332  demoivre  12333  demoivreALT  12334  odd2np1lem  12432  odd2np1  12433  opoe  12455  omoe  12456  opeo  12457  omeo  12458  modgcd  12561  qredeq  12667  modprm0  12826  pythagtriplem1  12837  pythagtriplem12  12847  pythagtriplem14  12849  gzmulcl  12950  4sqlem11  12973  4sqlem17  12979  cncrng  14582  cnfldmulg  14589  mpomulcn  15289  mulc1cncf  15312  mulcncflem  15330  dvmulxxbr  15425  dvmulxx  15427  dvimulf  15429  plymullem1  15471  plymulcl  15478  plysubcl  15479  efper  15530  sinperlem  15531  sin2kpi  15534  cos2kpi  15535  efimpi  15542  sincosq1eq  15562  abssinper  15569  sinkpi  15570  coskpi  15571  binom4  15702  fsumdvdsmul  15714  lgsdilem2  15764  lgsne0  15766  lgsquadlem1  15805  2sqlem2  15843