Theorem remulcl 9650

Description: Alias for ax-mulrcl 9628, for naming consistency with remulcli 9683. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
remulcl	|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

Proof of Theorem remulcl

Step	Hyp	Ref	Expression
1		ax-mulrcl 9628	1 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1898  (class class class)co 6315   RRcr 9564   x. cmul 9570

This theorem was proved from axioms:  ax-mulrcl 9628

This theorem is referenced by:  1re  9668  remulcli  9683  remulcld  9697  axmulgt0  9734  00id  9834  mul02lem1  9835  recextlem2  10271  recex  10272  lemul1  10485  ltmul12a  10489  lemul12b  10490  mulgt1  10492  mulge0b  10503  mulle0b  10504  ltdivmul  10508  ledivmul  10509  lt2mul2div  10511  lemuldiv  10514  ltdiv23  10525  lediv23  10526  supmullem2  10606  cju  10633  addltmul  10877  zmulcl  11014  irrmul  11318  rpnnen1lem1  11319  rpnnen1lem2  11320  rpnnen1lem3  11321  rpnnen1lem5  11323  rpmulcl  11353  xmulasslem3  11601  xadddilem  11609  ge0mulcl  11774  iccdil  11799  mulmod0  12136  modmulnn  12146  modidmul0OLD  12155  modcyc  12164  modmul1  12175  modaddmulmod  12188  moddi  12189  reexpcl  12321  reexpclz  12324  expge0  12340  expge1  12341  expubnd  12365  bernneq  12430  expmulnbnd  12436  digit2  12437  digit1  12438  discr  12441  faclbnd  12507  faclbnd3  12509  faclbnd5  12515  facavg  12518  cshweqrep  12957  crre  13226  remim  13229  mulre  13233  sqrlem6  13360  sqrlem7  13361  sqreulem  13471  amgm2  13481  o1mul  13727  caucvgrlem  13785  caucvgrlemOLD  13786  climcndslem2  13957  climcnds  13958  fprodrecl  14056  fprodreclf  14062  iprodrecl  14104  rerisefaccl  14119  refallfaccl  14120  efcllem  14181  ege2le3  14193  ef01bndlem  14287  cos01gt0  14294  modprm0  14805  prmreclem3  14911  4sqlem11  14948  resubdrg  19225  nmoco  21807  nghmco  21808  blcvx  21865  iihalf1  22008  iihalf2  22010  iimulcl  22014  pcoass  22104  tchcphlem1  22258  csbren  22402  trirn  22403  minveclem2  22417  minveclem2OLD  22429  sca2rab  22514  uniioombllem5  22594  mbfmulc2lem  22652  i1fmul  22703  i1fmulclem  22709  i1fmulc  22710  dveflem  22980  cmvth  22992  dvivthlem1  23009  dvfsumle  23022  dvfsumlem2  23028  pilem2  23456  pilem2OLD  23457  tangtx  23509  sinq12gt0  23511  coskpi  23524  cosne0  23528  efif1olem2  23541  efif1olem4  23543  relogexp  23594  logcxp  23663  rpcxpcl  23670  abscxpbnd  23742  ang180lem1  23787  atantan  23898  atanbndlem  23900  o1cxp  23949  divsqrtsumlem  23954  jensenlem2  23962  jensen  23963  zetacvg  23989  regamcl  24035  basellem1  24056  basellem4  24059  basellem9  24064  chtublem  24188  chtub  24189  logfaclbnd  24199  bpos1lem  24259  bposlem1  24261  bposlem2  24262  bposlem6  24266  bposlem7  24267  bposlem9  24269  lgseisen  24330  chebbnd1lem2  24357  chebbnd1lem3  24358  chto1ub  24363  rplogsumlem1  24371  dchrisumlem3  24378  dchrvmasumlem2  24385  dchrisum0lem1b  24402  dchrisum0lem1  24403  dchrisum0lem2  24405  mulog2sumlem1  24421  mulog2sumlem2  24422  log2sumbnd  24431  selberglem2  24433  chpdifbndlem1  24440  logdivbnd  24443  pntrlog2bndlem4  24467  pntibndlem2  24478  pntibndlem3  24479  pntlemh  24486  pntlemr  24489  pntlemk  24493  pntlemo  24494  ostth2lem1  24505  ostth2lem3  24522  ostth3  24525  axcontlem2  25044  nmoub3i  26463  blocni  26495  ubthlem3  26563  minvecolem2  26566  minvecolem2OLD  26576  bcs2  26884  nmopub2tALT  27611  nmfnleub2  27628  nmophmi  27733  bdophmi  27734  lnconi  27735  cnlnadjlem2  27770  cnlnadjlem7  27775  nmopadjlem  27791  nmopcoadji  27803  leopnmid  27840  cdj1i  28135  cdj3lem2b  28139  cdj3i  28143  addltmulALT  28148  pnfinf  28549  rezh  28824  sgnmul  29462  sgnmulsgn  29469  sgnmulsgp  29470  signshf  29526  dvtanlemOLD  32036  itg2addnclem  32038  ftc1anclem3  32064  isbnd2  32160  isbnd3  32161  equivbnd  32167  pellexlem5  35722  pell1234qrmulcl  35746  pellfundex  35779  rmspecsqrtnq  35799  jm2.24nn  35854  jm2.17a  35855  jm2.17b  35856  jm2.17c  35857  acongrep  35875  acongeq  35878  jm3.1lem2  35918  mulltgt0  37383  fmul01  37696  fmuldfeq  37699  fmul01lt1lem1  37700  fmul01lt1lem2  37701  stoweidlem3  37901  stoweidlem13  37911  stoweidlem17  37915  stoweidlem34  37933  stoweidlem42  37941  stoweidlem48  37947  fourierdlem83  38091  hoidmvlelem2  38456  2leaddle2  39086