Theorem mulcl 8149

Description: Alias for ax-mulcl 8120, for naming consistency with mulcli 8174. (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 8120	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 6013   CCcc 8020   x. cmul 8027

This theorem was proved from axioms:  ax-mulcl 8120

This theorem is referenced by:  mpomulf  8159  0cn  8161  mulrid  8166  mulcli  8174  mulcld  8190  mul31  8300  mul4  8301  muladd11r  8325  cnegexlem2  8345  cnegex  8347  muladd  8553  subdi  8554  mul02  8556  submul2  8568  mulsub  8570  recextlem1  8821  recexap  8823  muleqadd  8838  divassap  8860  divmulassap  8865  divmuldivap  8882  divmuleqap  8887  divadddivap  8897  conjmulap  8899  cju  9131  ofnegsub  9132  zneo  9571  exp3vallem  10792  exp3val  10793  exp1  10797  expp1  10798  expcl  10809  expclzaplem  10815  mulexp  10830  sqcl  10852  subsq  10898  subsq2  10899  binom2sub  10905  mulbinom2  10908  binom3  10909  zesq  10910  bernneq  10912  bernneq2  10913  mulsubdivbinom2ap  10963  facnn  10979  fac0  10980  fac1  10981  facp1  10982  bcval5  11015  bcn2  11016  reim  11403  imcl  11405  crre  11408  crim  11409  remim  11411  mulreap  11415  cjreb  11417  recj  11418  reneg  11419  readd  11420  remullem  11422  remul2  11424  imcj  11426  imneg  11427  imadd  11428  immul2  11431  cjadd  11435  ipcnval  11437  cjmulrcl  11438  cjneg  11441  imval2  11445  cjreim  11454  rennim  11553  sqabsadd  11606  sqabssub  11607  absreimsq  11618  absreim  11619  absmul  11620  mul0inf  11792  mulcn2  11863  climmul  11878  isermulc2  11891  fsummulc2  11999  prodf  12089  clim2prod  12090  clim2divap  12091  prod3fmul  12092  prodf1  12093  prodfap0  12096  prodfrecap  12097  prodrbdclem  12122  fproddccvg  12123  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  fprodntrivap  12135  prodsnf  12143  fprodcl  12158  fprodclf  12186  efexp  12233  sinf  12255  cosf  12256  tanval2ap  12264  tanval3ap  12265  resinval  12266  recosval  12267  efi4p  12268  resin4p  12269  recos4p  12270  resincl  12271  recoscl  12272  sinneg  12277  cosneg  12278  efival  12283  efmival  12284  efeul  12285  sinadd  12287  cosadd  12288  sinsub  12291  cossub  12292  subsin  12294  sinmul  12295  cosmul  12296  addcos  12297  subcos  12298  cos2tsin  12302  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  absef  12321  absefib  12322  efieq1re  12323  demoivre  12324  demoivreALT  12325  odd2np1lem  12423  odd2np1  12424  opoe  12446  omoe  12447  opeo  12448  omeo  12449  modgcd  12552  qredeq  12658  modprm0  12817  pythagtriplem1  12828  pythagtriplem12  12838  pythagtriplem14  12840  gzmulcl  12941  4sqlem11  12964  4sqlem17  12970  cncrng  14573  cnfldmulg  14580  mpomulcn  15280  mulc1cncf  15303  mulcncflem  15321  dvmulxxbr  15416  dvmulxx  15418  dvimulf  15420  plymullem1  15462  plymulcl  15469  plysubcl  15470  efper  15521  sinperlem  15522  sin2kpi  15525  cos2kpi  15526  efimpi  15533  sincosq1eq  15553  abssinper  15560  sinkpi  15561  coskpi  15562  binom4  15693  fsumdvdsmul  15705  lgsdilem2  15755  lgsne0  15757  lgsquadlem1  15796  2sqlem2  15834