Theorem remulcl 9623

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

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1870  (class class class)co 6305   RRcr 9537   x. cmul 9543

This theorem was proved from axioms:  ax-mulrcl 9601

This theorem is referenced by:  1re  9641  remulcli  9656  remulcld  9670  axmulgt0  9707  00id  9807  mul02lem1  9808  recextlem2  10242  recex  10243  lemul1  10456  ltmul12a  10460  lemul12b  10461  mulgt1  10463  mulge0b  10474  mulle0b  10475  ltdivmul  10479  ledivmul  10480  lt2mul2div  10482  lemuldiv  10485  ltdiv23  10497  lediv23  10498  supmullem2  10578  cju  10605  addltmul  10848  zmulcl  10985  irrmul  11289  rpnnen1lem1  11290  rpnnen1lem2  11291  rpnnen1lem3  11292  rpnnen1lem5  11294  rpmulcl  11324  xmulasslem3  11572  xadddilem  11580  ge0mulcl  11743  iccdil  11768  mulmod0  12101  modmulnn  12111  modidmul0OLD  12120  modcyc  12129  modmul1  12140  modaddmulmod  12153  moddi  12154  reexpcl  12286  reexpclz  12289  expge0  12305  expge1  12306  expubnd  12330  bernneq  12395  expmulnbnd  12401  digit2  12402  digit1  12403  discr  12406  faclbnd  12472  faclbnd3  12474  faclbnd5  12480  facavg  12483  cshweqrep  12905  crre  13156  remim  13159  mulre  13163  sqrlem6  13290  sqrlem7  13291  sqreulem  13401  amgm2  13411  o1mul  13656  caucvgrlem  13714  caucvgrlemOLD  13715  climcndslem2  13886  climcnds  13887  fprodrecl  13985  fprodreclf  13991  iprodrecl  14033  rerisefaccl  14048  refallfaccl  14049  efcllem  14110  ege2le3  14122  ef01bndlem  14216  cos01gt0  14223  modprm0  14719  prmreclem3  14825  4sqlem11  14862  resubdrg  19107  nmoco  21669  nghmco  21670  blcvx  21727  iihalf1  21855  iihalf2  21857  iimulcl  21861  pcoass  21948  tchcphlem1  22102  csbren  22246  trirn  22247  minveclem2  22261  sca2rab  22343  uniioombllem5  22422  mbfmulc2lem  22480  i1fmul  22531  i1fmulclem  22537  i1fmulc  22538  dveflem  22808  cmvth  22820  dvivthlem1  22837  dvfsumle  22850  dvfsumlem2  22856  pilem2  23272  pilem2OLD  23273  tangtx  23325  sinq12gt0  23327  coskpi  23340  cosne0  23344  efif1olem2  23357  efif1olem4  23359  relogexp  23410  logcxp  23479  rpcxpcl  23486  abscxpbnd  23558  ang180lem1  23603  atantan  23714  atanbndlem  23716  o1cxp  23765  divsqrtsumlem  23770  jensenlem2  23778  jensen  23779  zetacvg  23805  regamcl  23851  basellem1  23870  basellem4  23873  basellem9  23878  chtublem  24002  chtub  24003  logfaclbnd  24013  bpos1lem  24073  bposlem1  24075  bposlem2  24076  bposlem6  24080  bposlem7  24081  bposlem9  24083  lgseisen  24144  chebbnd1lem2  24171  chebbnd1lem3  24172  chto1ub  24177  rplogsumlem1  24185  dchrisumlem3  24192  dchrvmasumlem2  24199  dchrisum0lem1b  24216  dchrisum0lem1  24217  dchrisum0lem2  24219  mulog2sumlem1  24235  mulog2sumlem2  24236  log2sumbnd  24245  selberglem2  24247  chpdifbndlem1  24254  logdivbnd  24257  pntrlog2bndlem4  24281  pntibndlem2  24292  pntibndlem3  24293  pntlemh  24300  pntlemr  24303  pntlemk  24307  pntlemo  24308  ostth2lem1  24319  ostth2lem3  24336  ostth3  24339  axcontlem2  24841  nmoub3i  26259  blocni  26291  ubthlem3  26359  minvecolem2  26362  bcs2  26670  nmopub2tALT  27397  nmfnleub2  27414  nmophmi  27519  bdophmi  27520  lnconi  27521  cnlnadjlem2  27556  cnlnadjlem7  27561  nmopadjlem  27577  nmopcoadji  27589  leopnmid  27626  cdj1i  27921  cdj3lem2b  27925  cdj3i  27929  addltmulALT  27934  pnfinf  28338  rezh  28614  sgnmul  29201  sgnmulsgn  29208  sgnmulsgp  29209  signshf  29265  dvtanlemOLD  31695  itg2addnclem  31697  ftc1anclem3  31723  isbnd2  31819  isbnd3  31820  equivbnd  31826  pellexlem5  35387  pell1234qrmulcl  35409  pellfundex  35440  rmspecsqrtnq  35460  jm2.24nn  35515  jm2.17a  35516  jm2.17b  35517  jm2.17c  35518  acongrep  35536  acongeq  35539  jm3.1lem2  35579  mulltgt0  36983  fmul01  37230  fmuldfeq  37233  fmul01lt1lem1  37234  fmul01lt1lem2  37235  stoweidlem3  37432  stoweidlem13  37442  stoweidlem17  37446  stoweidlem34  37464  stoweidlem42  37472  stoweidlem48  37478  fourierdlem83  37621  2leaddle2  38393