Theorem mulcl 8254

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2203  (class class class)co 6050   CCcc 8125   x. cmul 8132

This theorem was proved from axioms:  ax-mulcl 8225

This theorem is referenced by:  mpomulf  8264  0cn  8266  mulrid  8271  mulcli  8279  mulcld  8294  mul31  8404  mul4  8405  muladd11r  8429  cnegexlem2  8449  cnegex  8451  muladd  8657  subdi  8658  mul02  8660  submul2  8672  mulsub  8674  recextlem1  8925  recexap  8927  muleqadd  8942  divassap  8964  divmulassap  8969  divmuldivap  8986  divmuleqap  8991  divadddivap  9001  conjmulap  9003  cju  9235  ofnegsub  9236  zneo  9679  exp3vallem  10902  exp3val  10903  exp1  10907  expp1  10908  expcl  10919  expclzaplem  10925  mulexp  10940  sqcl  10962  subsq  11008  subsq2  11009  binom2sub  11015  mulbinom2  11018  binom3  11019  zesq  11020  bernneq  11022  bernneq2  11023  mulsubdivbinom2ap  11073  facnn  11089  fac0  11090  fac1  11091  facp1  11092  bcval5  11125  bcn2  11126  reim  11537  imcl  11539  crre  11542  crim  11543  remim  11545  mulreap  11549  cjreb  11551  recj  11552  reneg  11553  readd  11554  remullem  11556  remul2  11558  imcj  11560  imneg  11561  imadd  11562  immul2  11565  cjadd  11569  ipcnval  11571  cjmulrcl  11572  cjneg  11575  imval2  11579  cjreim  11588  rennim  11687  sqabsadd  11740  sqabssub  11741  absreimsq  11752  absreim  11753  absmul  11754  mul0inf  11926  mulcn2  11997  climmul  12012  isermulc2  12025  fsummulc2  12134  prodf  12224  clim2prod  12225  clim2divap  12226  prod3fmul  12227  prodf1  12228  prodfap0  12231  prodfrecap  12232  prodrbdclem  12257  fproddccvg  12258  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  fprodntrivap  12270  prodsnf  12278  fprodcl  12293  fprodclf  12321  efexp  12368  sinf  12390  cosf  12391  tanval2ap  12399  tanval3ap  12400  resinval  12401  recosval  12402  efi4p  12403  resin4p  12404  recos4p  12405  resincl  12406  recoscl  12407  sinneg  12412  cosneg  12413  efival  12418  efmival  12419  efeul  12420  sinadd  12422  cosadd  12423  sinsub  12426  cossub  12427  subsin  12429  sinmul  12430  cosmul  12431  addcos  12432  subcos  12433  cos2tsin  12437  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  absef  12456  absefib  12457  efieq1re  12458  demoivre  12459  demoivreALT  12460  odd2np1lem  12558  odd2np1  12559  opoe  12581  omoe  12582  opeo  12583  omeo  12584  modgcd  12687  qredeq  12793  modprm0  12952  pythagtriplem1  12963  pythagtriplem12  12973  pythagtriplem14  12975  gzmulcl  13076  4sqlem11  13099  4sqlem17  13105  cncrng  14717  cnfldmulg  14724  mpomulcn  15431  mulc1cncf  15454  mulcncflem  15472  dvmulxxbr  15567  dvmulxx  15569  dvimulf  15571  plymullem1  15613  plymulcl  15620  plysubcl  15621  efper  15672  sinperlem  15673  sin2kpi  15676  cos2kpi  15677  efimpi  15684  sincosq1eq  15704  abssinper  15711  sinkpi  15712  coskpi  15713  binom4  15844  fsumdvdsmul  15859  lgsdilem2  15909  lgsne0  15911  lgsquadlem1  15950  2sqlem2  15988