Theorem remulcl 9594

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1819  (class class class)co 6296   RRcr 9508   x. cmul 9514

This theorem was proved from axioms:  ax-mulrcl 9572

This theorem is referenced by:  1re  9612  remulcli  9627  remulcld  9641  axmulgt0  9676  00id  9772  mul02lem1  9773  recextlem2  10201  recex  10202  lemul1  10415  ltmul12a  10419  lemul12b  10420  mulgt1  10422  mulge0b  10433  mulle0b  10434  ltdivmul  10438  ledivmul  10439  lt2mul2div  10441  lemuldiv  10444  ltdiv23  10456  lediv23  10457  supmullem2  10530  cju  10552  addltmul  10795  zmulcl  10933  irrmul  11232  rpnnen1lem1  11233  rpnnen1lem2  11234  rpnnen1lem3  11235  rpnnen1lem5  11237  rpmulcl  11266  xmulasslem3  11503  xadddilem  11511  ge0mulcl  11658  iccdil  11683  modmulnn  12015  modidmul0  12024  modcyc  12033  modmul1  12042  modaddmulmod  12055  moddi  12056  reexpcl  12185  reexpclz  12188  expge0  12204  expge1  12205  expubnd  12228  bernneq  12294  expmulnbnd  12300  digit2  12301  digit1  12302  discr  12305  faclbnd  12370  faclbnd3  12372  faclbnd5  12378  facavg  12381  cshweqrep  12800  crre  12958  remim  12961  mulre  12965  sqrlem6  13092  sqrlem7  13093  sqreulem  13203  amgm2  13213  o1mul  13448  caucvgrlem  13506  climcndslem2  13673  climcnds  13674  fprodrecl  13771  iprodrecl  13806  efcllem  13824  ege2le3  13836  ef01bndlem  13930  cos01gt0  13937  modprm0  14341  prmreclem3  14447  4sqlem11  14484  resubdrg  18770  nmoco  21369  nghmco  21370  blcvx  21428  iihalf1  21556  iihalf2  21558  iimulcl  21562  pcoass  21649  tchcphlem1  21803  csbren  21951  trirn  21952  minveclem2  21966  sca2rab  22048  uniioombllem5  22121  mbfmulc2lem  22179  i1fmul  22228  i1fmulclem  22234  i1fmulc  22235  dveflem  22505  cmvth  22517  dvivthlem1  22534  dvfsumle  22547  dvfsumlem2  22553  pilem2  22972  tangtx  23023  sinq12gt0  23025  coskpi  23038  cosne0  23042  efif1olem2  23055  efif1olem4  23057  relogexp  23105  logcxp  23175  rpcxpcl  23182  abscxpbnd  23252  ang180lem1  23266  atantan  23379  atanbndlem  23381  o1cxp  23429  divsqrtsumlem  23434  jensenlem2  23442  jensen  23443  basellem1  23479  basellem4  23482  basellem9  23487  chtublem  23611  chtub  23612  logfaclbnd  23622  bpos1lem  23682  bposlem1  23684  bposlem2  23685  bposlem6  23689  bposlem7  23690  bposlem9  23692  lgseisen  23753  chebbnd1lem2  23780  chebbnd1lem3  23781  chto1ub  23786  rplogsumlem1  23794  dchrisumlem3  23801  dchrvmasumlem2  23808  dchrisum0lem1b  23825  dchrisum0lem1  23826  dchrisum0lem2  23828  mulog2sumlem1  23844  mulog2sumlem2  23845  log2sumbnd  23854  selberglem2  23856  chpdifbndlem1  23863  logdivbnd  23866  pntrlog2bndlem4  23890  pntibndlem2  23901  pntibndlem3  23902  pntlemh  23909  pntlemr  23912  pntlemk  23916  pntlemo  23917  ostth2lem1  23928  ostth2lem3  23945  ostth3  23948  axcontlem2  24394  nmoub3i  25814  blocni  25846  ubthlem3  25914  minvecolem2  25917  bcs2  26225  nmopub2tALT  26954  nmfnleub2  26971  nmophmi  27076  bdophmi  27077  lnconi  27078  cnlnadjlem2  27113  cnlnadjlem7  27118  nmopadjlem  27134  nmopcoadji  27146  leopnmid  27183  cdj1i  27478  cdj3lem2b  27482  cdj3i  27486  addltmulALT  27491  pnfinf  27879  rezh  28105  sgnmul  28656  sgnmulsgn  28663  sgnmulsgp  28664  signshf  28720  zetacvg  28732  regamcl  28778  rerisefaccl  29314  refallfaccl  29315  dvtanlem  30226  itg2addnclem  30228  ftc1anclem3  30254  isbnd2  30441  isbnd3  30442  equivbnd  30448  pellexlem5  30931  pell1234qrmulcl  30953  pellfundex  30984  rmspecsqrtnq  31004  jm2.24nn  31059  jm2.17a  31060  jm2.17b  31061  jm2.17c  31062  acongrep  31080  acongeq  31083  jm3.1lem2  31122  mulltgt0  31558  fmul01  31735  fmuldfeq  31738  fmul01lt1lem1  31739  fmul01lt1lem2  31740  fprodreclf  31757  stoweidlem3  31946  stoweidlem13  31956  stoweidlem17  31960  stoweidlem34  31977  stoweidlem42  31985  stoweidlem48  31991  fourierdlem83  32133  2leaddle2  32542