Theorem remulcl 9481

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1758  (class class class)co 6203   RRcr 9395   x. cmul 9401

This theorem was proved from axioms:  ax-mulrcl 9459

This theorem is referenced by:  1re  9499  remulcli  9514  remulcld  9528  axmulgt0  9563  00id  9658  mul02lem1  9659  recextlem2  10081  recex  10082  lemul1  10295  ltmul12a  10299  lemul12b  10300  mulgt1  10302  mulge0b  10313  mulle0b  10314  ltdivmul  10318  ledivmul  10319  ledivmulOLD  10320  lt2mul2div  10322  lemuldiv  10325  ltdiv23  10337  lediv23  10338  supmullem2  10411  cju  10432  addltmul  10674  zmulcl  10807  irrmul  11092  rpnnen1lem1  11093  rpnnen1lem2  11094  rpnnen1lem3  11095  rpnnen1lem5  11097  rpmulcl  11126  xmulasslem3  11363  xadddilem  11371  ge0mulcl  11518  iccdil  11543  modmulnn  11845  modidmul0  11854  modcyc  11863  modmul1  11872  modaddmulmod  11885  moddi  11886  reexpcl  12002  reexpclz  12005  expge0  12020  expge1  12021  expubnd  12044  bernneq  12110  expmulnbnd  12116  digit2  12117  digit1  12118  discr  12121  faclbnd  12186  faclbnd3  12188  faclbnd5  12194  facavg  12197  cshweqrep  12576  crre  12724  remim  12727  mulre  12731  sqrlem6  12858  sqrlem7  12859  sqreulem  12968  amgm2  12978  o1mul  13213  caucvgrlem  13271  climcndslem2  13434  climcnds  13435  efcllem  13484  ege2le3  13496  ef01bndlem  13589  cos01gt0  13596  modprm0  13994  prmreclem3  14100  4sqlem11  14137  resubdrg  18166  nmoco  20451  nghmco  20452  blcvx  20510  iihalf1  20638  iihalf2  20640  iimulcl  20644  pcoass  20731  tchcphlem1  20885  csbren  21033  trirn  21034  minveclem2  21048  sca2rab  21130  uniioombllem5  21203  mbfmulc2lem  21261  i1fmul  21310  i1fmulclem  21316  i1fmulc  21317  dveflem  21587  cmvth  21599  dvivthlem1  21616  dvfsumle  21629  dvfsumlem2  21635  pilem2  22053  tangtx  22103  sinq12gt0  22105  coskpi  22118  cosne0  22122  efif1olem2  22135  efif1olem4  22137  relogexp  22180  logcxp  22250  rpcxpcl  22257  abscxpbnd  22327  ang180lem1  22341  atantan  22454  atanbndlem  22456  o1cxp  22504  divsqrsumlem  22509  jensenlem2  22517  jensen  22518  basellem1  22554  basellem4  22557  basellem9  22562  chtublem  22686  chtub  22687  logfaclbnd  22697  bpos1lem  22757  bposlem1  22759  bposlem2  22760  bposlem6  22764  bposlem7  22765  bposlem9  22767  lgseisen  22828  chebbnd1lem2  22855  chebbnd1lem3  22856  chto1ub  22861  rplogsumlem1  22869  dchrisumlem3  22876  dchrvmasumlem2  22883  dchrisum0lem1b  22900  dchrisum0lem1  22901  dchrisum0lem2  22903  mulog2sumlem1  22919  mulog2sumlem2  22920  log2sumbnd  22929  selberglem2  22931  chpdifbndlem1  22938  logdivbnd  22941  pntrlog2bndlem4  22965  pntibndlem2  22976  pntibndlem3  22977  pntlemh  22984  pntlemr  22987  pntlemk  22991  pntlemo  22992  ostth2lem1  23003  ostth2lem3  23020  ostth3  23023  axcontlem2  23383  nmoub3i  24345  blocni  24377  ubthlem3  24445  minvecolem2  24448  bcs2  24756  nmopub2tALT  25485  nmfnleub2  25502  nmophmi  25607  bdophmi  25608  lnconi  25609  cnlnadjlem2  25644  cnlnadjlem7  25649  nmopadjlem  25665  nmopcoadji  25677  leopnmid  25714  cdj1i  26009  cdj3lem2b  26013  cdj3i  26017  addltmulALT  26022  pnfinf  26365  rezh  26565  sgnmul  27089  sgnmulsgn  27096  sgnmulsgp  27097  signshf  27153  zetacvg  27165  regamcl  27211  fprodrecl  27630  iprodrecl  27666  rerisefaccl  27684  refallfaccl  27685  dvtanlem  28609  itg2addnclem  28611  ftc1anclem3  28637  isbnd2  28850  isbnd3  28851  equivbnd  28857  pellexlem5  29342  pell1234qrmulcl  29364  pellfundex  29395  rmspecsqrnq  29415  jm2.24nn  29470  jm2.17a  29471  jm2.17b  29472  jm2.17c  29473  acongrep  29491  acongeq  29494  jm3.1lem2  29535  mulltgt0  29912  fmul01  29929  fmuldfeq  29932  fmul01lt1lem1  29933  fmul01lt1lem2  29934  stoweidlem3  29966  stoweidlem13  29976  stoweidlem17  29980  stoweidlem34  29997  stoweidlem42  30005  stoweidlem48  30011  2leaddle2  30343