Theorem remulcl 9355

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1755  (class class class)co 6080   RRcr 9269   x. cmul 9275

This theorem was proved from axioms:  ax-mulrcl 9333

This theorem is referenced by:  1re  9373  remulcli  9388  remulcld  9402  axmulgt0  9437  00id  9532  mul02lem1  9533  recextlem2  9955  recex  9956  lemul1  10169  ltmul12a  10173  lemul12b  10174  mulgt1  10176  mulge0b  10187  mulle0b  10188  ltdivmul  10192  ledivmul  10193  ledivmulOLD  10194  lt2mul2div  10196  lemuldiv  10199  ltdiv23  10211  lediv23  10212  supmullem2  10285  cju  10306  addltmul  10548  zmulcl  10681  irrmul  10966  rpnnen1lem1  10967  rpnnen1lem2  10968  rpnnen1lem3  10969  rpnnen1lem5  10971  rpmulcl  11000  xmulasslem3  11237  xadddilem  11245  ge0mulcl  11385  iccdil  11410  modmulnn  11709  modidmul0  11718  modcyc  11727  modmul1  11736  modaddmulmod  11749  moddi  11750  reexpcl  11866  reexpclz  11869  expge0  11884  expge1  11885  expubnd  11908  bernneq  11974  expmulnbnd  11980  digit2  11981  digit1  11982  discr  11985  faclbnd  12050  faclbnd3  12052  faclbnd5  12058  facavg  12061  cshweqrep  12439  crre  12587  remim  12590  mulre  12594  sqrlem6  12721  sqrlem7  12722  sqreulem  12831  amgm2  12841  o1mul  13076  caucvgrlem  13134  climcndslem2  13296  climcnds  13297  efcllem  13346  ege2le3  13358  ef01bndlem  13451  cos01gt0  13458  modprm0  13856  prmreclem3  13962  4sqlem11  13999  resubdrg  17880  nmoco  20158  nghmco  20159  blcvx  20217  iihalf1  20345  iihalf2  20347  iimulcl  20351  pcoass  20438  tchcphlem1  20592  csbren  20740  trirn  20741  minveclem2  20755  sca2rab  20837  uniioombllem5  20909  mbfmulc2lem  20967  i1fmul  21016  i1fmulclem  21022  i1fmulc  21023  dveflem  21293  cmvth  21305  dvivthlem1  21322  dvfsumle  21335  dvfsumlem2  21341  pilem2  21802  tangtx  21852  sinq12gt0  21854  coskpi  21867  cosne0  21871  efif1olem2  21884  efif1olem4  21886  relogexp  21929  logcxp  21999  rpcxpcl  22006  abscxpbnd  22076  ang180lem1  22090  atantan  22203  atanbndlem  22205  o1cxp  22253  divsqrsumlem  22258  jensenlem2  22266  jensen  22267  basellem1  22303  basellem4  22306  basellem9  22311  chtublem  22435  chtub  22436  logfaclbnd  22446  bpos1lem  22506  bposlem1  22508  bposlem2  22509  bposlem6  22513  bposlem7  22514  bposlem9  22516  lgseisen  22577  chebbnd1lem2  22604  chebbnd1lem3  22605  chto1ub  22610  rplogsumlem1  22618  dchrisumlem3  22625  dchrvmasumlem2  22632  dchrisum0lem1b  22649  dchrisum0lem1  22650  dchrisum0lem2  22652  mulog2sumlem1  22668  mulog2sumlem2  22669  log2sumbnd  22678  selberglem2  22680  chpdifbndlem1  22687  logdivbnd  22690  pntrlog2bndlem4  22714  pntibndlem2  22725  pntibndlem3  22726  pntlemh  22733  pntlemr  22736  pntlemk  22740  pntlemo  22741  ostth2lem1  22752  ostth2lem3  22769  ostth3  22772  axcontlem2  23034  nmoub3i  23996  blocni  24028  ubthlem3  24096  minvecolem2  24099  bcs2  24407  nmopub2tALT  25136  nmfnleub2  25153  nmophmi  25258  bdophmi  25259  lnconi  25260  cnlnadjlem2  25295  cnlnadjlem7  25300  nmopadjlem  25316  nmopcoadji  25328  leopnmid  25365  cdj1i  25660  cdj3lem2b  25664  cdj3i  25668  addltmulALT  25673  pnfinf  26024  rezh  26254  sgnmul  26773  sgnmulsgn  26780  sgnmulsgp  26781  signshf  26837  zetacvg  26849  regamcl  26895  fprodrecl  27313  iprodrecl  27349  rerisefaccl  27367  refallfaccl  27368  dvtanlem  28285  itg2addnclem  28287  ftc1anclem3  28313  isbnd2  28526  isbnd3  28527  equivbnd  28533  pellexlem5  29019  pell1234qrmulcl  29041  pellfundex  29072  rmspecsqrnq  29092  jm2.24nn  29147  jm2.17a  29148  jm2.17b  29149  jm2.17c  29150  acongrep  29168  acongeq  29171  jm3.1lem2  29212  mulltgt0  29589  fmul01  29606  fmuldfeq  29609  fmul01lt1lem1  29610  fmul01lt1lem2  29611  stoweidlem3  29644  stoweidlem13  29654  stoweidlem17  29658  stoweidlem34  29675  stoweidlem42  29683  stoweidlem48  29689  2leaddle2  30021