Theorem remulcl 9031

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

Syntax hints:   -> wi 4   /\ wa 359   e. wcel 1721  (class class class)co 6040   RRcr 8945   x. cmul 8951

This theorem is referenced by:  1re  9046  remulcli  9060  remulcld  9072  axmulgt0  9106  00id  9197  mul02lem1  9198  recextlem2  9609  recex  9610  lemul1  9818  ltmul12a  9822  lemul12b  9823  mulgt1  9825  ltdivmul  9838  ledivmul  9839  ledivmulOLD  9840  lt2mul2div  9842  lemuldiv  9845  ltdiv23  9857  lediv23  9858  supmullem2  9931  cju  9952  addltmul  10159  zmulcl  10280  irrmul  10555  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  rpmulcl  10589  xmulasslem3  10821  xadddilem  10829  ge0mulcl  10966  iccdil  10990  modmulnn  11220  modcyc  11231  modmul1  11234  moddi  11239  reexpcl  11353  reexpclz  11356  expge0  11371  expge1  11372  expubnd  11395  bernneq  11460  expmulnbnd  11466  digit2  11467  digit1  11468  discr  11471  faclbnd  11536  faclbnd3  11538  faclbnd5  11544  facavg  11547  crre  11874  remim  11877  mulre  11881  sqrlem6  12008  sqrlem7  12009  sqreulem  12118  amgm2  12128  o1mul  12363  caucvgrlem  12421  climcndslem2  12585  climcnds  12586  efcllem  12635  ege2le3  12647  ef01bndlem  12740  cos01gt0  12747  prmreclem3  13241  4sqlem11  13278  resubdrg  16705  nmoco  18724  nghmco  18725  blcvx  18782  iihalf1  18909  iihalf2  18911  iimulcl  18915  pcoass  19002  tchcphlem1  19145  minveclem2  19280  sca2rab  19361  uniioombllem5  19432  mbfmulc2lem  19492  i1fmul  19541  i1fmulclem  19547  i1fmulc  19548  dveflem  19816  cmvth  19828  dvivthlem1  19845  dvfsumle  19858  dvfsumlem2  19864  pilem2  20321  tangtx  20366  sinq12gt0  20368  coskpi  20381  cosne0  20385  efif1olem2  20398  efif1olem4  20400  relogexp  20443  logcxp  20513  rpcxpcl  20520  abscxpbnd  20590  ang180lem1  20604  atantan  20716  atanbndlem  20718  o1cxp  20766  divsqrsumlem  20771  jensenlem2  20779  jensen  20780  basellem1  20816  basellem4  20819  basellem9  20824  chtublem  20948  chtub  20949  logfaclbnd  20959  bpos1lem  21019  bposlem1  21021  bposlem2  21022  bposlem6  21026  bposlem7  21027  bposlem9  21029  lgseisen  21090  chebbnd1lem2  21117  chebbnd1lem3  21118  chto1ub  21123  rplogsumlem1  21131  dchrisumlem3  21138  dchrvmasumlem2  21145  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2  21165  mulog2sumlem1  21181  mulog2sumlem2  21182  log2sumbnd  21191  selberglem2  21193  chpdifbndlem1  21200  logdivbnd  21203  pntrlog2bndlem4  21227  pntibndlem2  21238  pntibndlem3  21239  pntlemh  21246  pntlemr  21249  pntlemk  21253  pntlemo  21254  ostth2lem1  21265  ostth2lem3  21282  ostth3  21285  nmoub3i  22227  blocni  22259  ubthlem3  22327  minvecolem2  22330  bcs2  22637  nmopub2tALT  23365  nmfnleub2  23382  nmophmi  23487  bdophmi  23488  lnconi  23489  cnlnadjlem2  23524  cnlnadjlem7  23529  nmopadjlem  23545  nmopcoadji  23557  leopnmid  23594  cdj1i  23889  cdj3lem2b  23893  cdj3i  23897  addltmulALT  23902  pnfinf  24206  rezh  24308  zetacvg  24752  regamcl  24798  mulge0b  25144  mulle0b  25145  fprodrecl  25232  iprodrecl  25268  rerisefaccl  25285  refallfaccl  25286  axcontlem2  25808  itg2addnclem  26155  csbrn  26346  trirn  26347  isbnd2  26382  isbnd3  26383  equivbnd  26389  pellexlem5  26786  pell1234qrmulcl  26808  pellfundex  26839  rmspecsqrnq  26859  jm2.24nn  26914  jm2.17a  26915  jm2.17b  26916  jm2.17c  26917  acongrep  26935  acongeq  26938  jm3.1lem2  26979  mulltgt0  27560  fmul01  27577  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  stoweidlem3  27619  stoweidlem13  27629  stoweidlem17  27633  stoweidlem34  27650  stoweidlem42  27658  stoweidlem48  27664

This theorem was proved from axioms:  ax-mulrcl 9009