Theorem remulcl 9359

Description: Alias for ax-mulrcl 9337, for naming consistency with remulcli 9392. (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 9337	1 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1756  (class class class)co 6086   RRcr 9273   x. cmul 9279

This theorem was proved from axioms:  ax-mulrcl 9337

This theorem is referenced by:  1re  9377  remulcli  9392  remulcld  9406  axmulgt0  9441  00id  9536  mul02lem1  9537  recextlem2  9959  recex  9960  lemul1  10173  ltmul12a  10177  lemul12b  10178  mulgt1  10180  mulge0b  10191  mulle0b  10192  ltdivmul  10196  ledivmul  10197  ledivmulOLD  10198  lt2mul2div  10200  lemuldiv  10203  ltdiv23  10215  lediv23  10216  supmullem2  10289  cju  10310  addltmul  10552  zmulcl  10685  irrmul  10970  rpnnen1lem1  10971  rpnnen1lem2  10972  rpnnen1lem3  10973  rpnnen1lem5  10975  rpmulcl  11004  xmulasslem3  11241  xadddilem  11249  ge0mulcl  11390  iccdil  11415  modmulnn  11717  modidmul0  11726  modcyc  11735  modmul1  11744  modaddmulmod  11757  moddi  11758  reexpcl  11874  reexpclz  11877  expge0  11892  expge1  11893  expubnd  11916  bernneq  11982  expmulnbnd  11988  digit2  11989  digit1  11990  discr  11993  faclbnd  12058  faclbnd3  12060  faclbnd5  12066  facavg  12069  cshweqrep  12447  crre  12595  remim  12598  mulre  12602  sqrlem6  12729  sqrlem7  12730  sqreulem  12839  amgm2  12849  o1mul  13084  caucvgrlem  13142  climcndslem2  13305  climcnds  13306  efcllem  13355  ege2le3  13367  ef01bndlem  13460  cos01gt0  13467  modprm0  13865  prmreclem3  13971  4sqlem11  14008  resubdrg  18013  nmoco  20291  nghmco  20292  blcvx  20350  iihalf1  20478  iihalf2  20480  iimulcl  20484  pcoass  20571  tchcphlem1  20725  csbren  20873  trirn  20874  minveclem2  20888  sca2rab  20970  uniioombllem5  21042  mbfmulc2lem  21100  i1fmul  21149  i1fmulclem  21155  i1fmulc  21156  dveflem  21426  cmvth  21438  dvivthlem1  21455  dvfsumle  21468  dvfsumlem2  21474  pilem2  21892  tangtx  21942  sinq12gt0  21944  coskpi  21957  cosne0  21961  efif1olem2  21974  efif1olem4  21976  relogexp  22019  logcxp  22089  rpcxpcl  22096  abscxpbnd  22166  ang180lem1  22180  atantan  22293  atanbndlem  22295  o1cxp  22343  divsqrsumlem  22348  jensenlem2  22356  jensen  22357  basellem1  22393  basellem4  22396  basellem9  22401  chtublem  22525  chtub  22526  logfaclbnd  22536  bpos1lem  22596  bposlem1  22598  bposlem2  22599  bposlem6  22603  bposlem7  22604  bposlem9  22606  lgseisen  22667  chebbnd1lem2  22694  chebbnd1lem3  22695  chto1ub  22700  rplogsumlem1  22708  dchrisumlem3  22715  dchrvmasumlem2  22722  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2  22742  mulog2sumlem1  22758  mulog2sumlem2  22759  log2sumbnd  22768  selberglem2  22770  chpdifbndlem1  22777  logdivbnd  22780  pntrlog2bndlem4  22804  pntibndlem2  22815  pntibndlem3  22816  pntlemh  22823  pntlemr  22826  pntlemk  22830  pntlemo  22831  ostth2lem1  22842  ostth2lem3  22859  ostth3  22862  axcontlem2  23162  nmoub3i  24124  blocni  24156  ubthlem3  24224  minvecolem2  24227  bcs2  24535  nmopub2tALT  25264  nmfnleub2  25281  nmophmi  25386  bdophmi  25387  lnconi  25388  cnlnadjlem2  25423  cnlnadjlem7  25428  nmopadjlem  25444  nmopcoadji  25456  leopnmid  25493  cdj1i  25788  cdj3lem2b  25792  cdj3i  25796  addltmulALT  25801  pnfinf  26151  rezh  26352  sgnmul  26877  sgnmulsgn  26884  sgnmulsgp  26885  signshf  26941  zetacvg  26953  regamcl  26999  fprodrecl  27417  iprodrecl  27453  rerisefaccl  27471  refallfaccl  27472  dvtanlem  28394  itg2addnclem  28396  ftc1anclem3  28422  isbnd2  28635  isbnd3  28636  equivbnd  28642  pellexlem5  29127  pell1234qrmulcl  29149  pellfundex  29180  rmspecsqrnq  29200  jm2.24nn  29255  jm2.17a  29256  jm2.17b  29257  jm2.17c  29258  acongrep  29276  acongeq  29279  jm3.1lem2  29320  mulltgt0  29697  fmul01  29714  fmuldfeq  29717  fmul01lt1lem1  29718  fmul01lt1lem2  29719  stoweidlem3  29751  stoweidlem13  29761  stoweidlem17  29765  stoweidlem34  29782  stoweidlem42  29790  stoweidlem48  29796  2leaddle2  30128