Theorem remulcl 9576

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1767  (class class class)co 6283   RRcr 9490   x. cmul 9496

This theorem was proved from axioms:  ax-mulrcl 9554

This theorem is referenced by:  1re  9594  remulcli  9609  remulcld  9623  axmulgt0  9658  00id  9753  mul02lem1  9754  recextlem2  10179  recex  10180  lemul1  10393  ltmul12a  10397  lemul12b  10398  mulgt1  10400  mulge0b  10411  mulle0b  10412  ltdivmul  10416  ledivmul  10417  ledivmulOLD  10418  lt2mul2div  10420  lemuldiv  10423  ltdiv23  10435  lediv23  10436  supmullem2  10509  cju  10531  addltmul  10773  zmulcl  10910  irrmul  11206  rpnnen1lem1  11207  rpnnen1lem2  11208  rpnnen1lem3  11209  rpnnen1lem5  11211  rpmulcl  11240  xmulasslem3  11477  xadddilem  11485  ge0mulcl  11632  iccdil  11657  modmulnn  11980  modidmul0  11989  modcyc  11998  modmul1  12007  modaddmulmod  12020  moddi  12021  reexpcl  12150  reexpclz  12153  expge0  12169  expge1  12170  expubnd  12193  bernneq  12259  expmulnbnd  12265  digit2  12266  digit1  12267  discr  12270  faclbnd  12335  faclbnd3  12337  faclbnd5  12343  facavg  12346  cshweqrep  12751  crre  12909  remim  12912  mulre  12916  sqrlem6  13043  sqrlem7  13044  sqreulem  13154  amgm2  13164  o1mul  13399  caucvgrlem  13457  climcndslem2  13624  climcnds  13625  efcllem  13674  ege2le3  13686  ef01bndlem  13779  cos01gt0  13786  modprm0  14188  prmreclem3  14294  4sqlem11  14331  resubdrg  18427  nmoco  20995  nghmco  20996  blcvx  21054  iihalf1  21182  iihalf2  21184  iimulcl  21188  pcoass  21275  tchcphlem1  21429  csbren  21577  trirn  21578  minveclem2  21592  sca2rab  21674  uniioombllem5  21747  mbfmulc2lem  21805  i1fmul  21854  i1fmulclem  21860  i1fmulc  21861  dveflem  22131  cmvth  22143  dvivthlem1  22160  dvfsumle  22173  dvfsumlem2  22179  pilem2  22597  tangtx  22647  sinq12gt0  22649  coskpi  22662  cosne0  22666  efif1olem2  22679  efif1olem4  22681  relogexp  22724  logcxp  22794  rpcxpcl  22801  abscxpbnd  22871  ang180lem1  22885  atantan  22998  atanbndlem  23000  o1cxp  23048  divsqrtsumlem  23053  jensenlem2  23061  jensen  23062  basellem1  23098  basellem4  23101  basellem9  23106  chtublem  23230  chtub  23231  logfaclbnd  23241  bpos1lem  23301  bposlem1  23303  bposlem2  23304  bposlem6  23308  bposlem7  23309  bposlem9  23311  lgseisen  23372  chebbnd1lem2  23399  chebbnd1lem3  23400  chto1ub  23405  rplogsumlem1  23413  dchrisumlem3  23420  dchrvmasumlem2  23427  dchrisum0lem1b  23444  dchrisum0lem1  23445  dchrisum0lem2  23447  mulog2sumlem1  23463  mulog2sumlem2  23464  log2sumbnd  23473  selberglem2  23475  chpdifbndlem1  23482  logdivbnd  23485  pntrlog2bndlem4  23509  pntibndlem2  23520  pntibndlem3  23521  pntlemh  23528  pntlemr  23531  pntlemk  23535  pntlemo  23536  ostth2lem1  23547  ostth2lem3  23564  ostth3  23567  axcontlem2  23960  nmoub3i  25380  blocni  25412  ubthlem3  25480  minvecolem2  25483  bcs2  25791  nmopub2tALT  26520  nmfnleub2  26537  nmophmi  26642  bdophmi  26643  lnconi  26644  cnlnadjlem2  26679  cnlnadjlem7  26684  nmopadjlem  26700  nmopcoadji  26712  leopnmid  26749  cdj1i  27044  cdj3lem2b  27048  cdj3i  27052  addltmulALT  27057  pnfinf  27405  rezh  27604  sgnmul  28137  sgnmulsgn  28144  sgnmulsgp  28145  signshf  28201  zetacvg  28213  regamcl  28259  fprodrecl  28678  iprodrecl  28714  rerisefaccl  28732  refallfaccl  28733  dvtanlem  29657  itg2addnclem  29659  ftc1anclem3  29685  isbnd2  29898  isbnd3  29899  equivbnd  29905  pellexlem5  30389  pell1234qrmulcl  30411  pellfundex  30442  rmspecsqrtnq  30462  jm2.24nn  30517  jm2.17a  30518  jm2.17b  30519  jm2.17c  30520  acongrep  30538  acongeq  30541  jm3.1lem2  30580  mulltgt0  30991  fmul01  31146  fmuldfeq  31149  fmul01lt1lem1  31150  fmul01lt1lem2  31151  ioodvbdlimc1lem1  31277  ioodvbdlimc2lem  31280  stoweidlem3  31319  stoweidlem13  31329  stoweidlem17  31333  stoweidlem34  31350  stoweidlem42  31358  stoweidlem48  31364  dirkercncflem2  31420  fourierdlem6  31429  fourierdlem26  31449  fourierdlem35  31458  fourierdlem39  31462  fourierdlem43  31466  fourierdlem45  31468  fourierdlem57  31480  fourierdlem62  31485  fourierdlem66  31489  fourierdlem78  31501  fourierdlem83  31506  fourierdlem112  31535  2leaddle2  31803