MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  remulcl Unicode version

Theorem remulcl 8912
Description: Alias for ax-mulrcl 8890, for naming consistency with remulcli 8941. (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
StepHypRef Expression
1 ax-mulrcl 8890 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1710  (class class class)co 5945   RRcr 8826    x. cmul 8832
This theorem is referenced by:  1re  8927  remulcli  8941  remulcld  8953  axmulgt0  8987  00id  9077  mul02lem1  9078  recextlem2  9489  recex  9490  lemul1  9698  ltmul12a  9702  lemul12b  9703  mulgt1  9705  ltdivmul  9718  ledivmul  9719  ledivmulOLD  9720  lt2mul2div  9722  lemuldiv  9725  ltdiv23  9737  lediv23  9738  supmullem2  9811  cju  9832  addltmul  10039  zmulcl  10158  irrmul  10433  rpnnen1lem1  10434  rpnnen1lem2  10435  rpnnen1lem3  10436  rpnnen1lem5  10438  rpmulcl  10467  xmulasslem3  10698  xadddilem  10706  ge0mulcl  10841  iccdil  10865  modmulnn  11080  modcyc  11091  modmul1  11094  moddi  11099  reexpcl  11213  reexpclz  11216  expge0  11231  expge1  11232  expubnd  11255  bernneq  11320  expmulnbnd  11326  digit2  11327  digit1  11328  discr  11331  faclbnd  11396  faclbnd3  11398  faclbnd5  11404  facavg  11407  crre  11695  remim  11698  mulre  11702  sqrlem6  11829  sqrlem7  11830  sqreulem  11939  amgm2  11949  o1mul  12184  caucvgrlem  12242  climcndslem2  12406  climcnds  12407  efcllem  12456  ege2le3  12468  ef01bndlem  12561  cos01gt0  12568  prmreclem3  13062  4sqlem11  13099  resubdrg  16529  nmoco  18348  nghmco  18349  blcvx  18406  iihalf1  18533  iihalf2  18535  iimulcl  18539  pcoass  18626  tchcphlem1  18769  minveclem2  18894  sca2rab  18975  uniioombllem5  19046  mbfmulc2lem  19106  i1fmul  19155  i1fmulclem  19161  i1fmulc  19162  dveflem  19430  cmvth  19442  dvivthlem1  19459  dvfsumle  19472  dvfsumlem2  19478  pilem2  19935  tangtx  19980  sinq12gt0  19982  coskpi  19995  cosne0  19999  efif1olem2  20012  efif1olem4  20014  relogexp  20057  logcxp  20127  rpcxpcl  20134  abscxpbnd  20204  ang180lem1  20218  atantan  20330  atanbndlem  20332  o1cxp  20380  divsqrsumlem  20385  jensenlem2  20393  jensen  20394  basellem1  20430  basellem4  20433  basellem9  20438  chtublem  20562  chtub  20563  logfaclbnd  20573  bpos1lem  20633  bposlem1  20635  bposlem2  20636  bposlem6  20640  bposlem7  20641  bposlem9  20643  lgseisen  20704  chebbnd1lem2  20731  chebbnd1lem3  20732  chto1ub  20737  rplogsumlem1  20745  dchrisumlem3  20752  dchrvmasumlem2  20759  dchrisum0lem1b  20776  dchrisum0lem1  20777  dchrisum0lem2  20779  mulog2sumlem1  20795  mulog2sumlem2  20796  log2sumbnd  20805  selberglem2  20807  chpdifbndlem1  20814  logdivbnd  20817  pntrlog2bndlem4  20841  pntibndlem2  20852  pntibndlem3  20853  pntlemh  20860  pntlemr  20863  pntlemk  20867  pntlemo  20868  ostth2lem1  20879  ostth2lem3  20896  ostth3  20899  nmoub3i  21465  blocni  21497  ubthlem3  21565  minvecolem2  21568  bcs2  21875  nmopub2tALT  22603  nmfnleub2  22620  nmophmi  22725  bdophmi  22726  lnconi  22727  cnlnadjlem2  22762  cnlnadjlem7  22767  nmopadjlem  22783  nmopcoadji  22795  leopnmid  22832  cdj1i  23127  cdj3lem2b  23131  cdj3i  23135  addltmulALT  23140  zetacvg  24048  regamcl  24094  mulge0b  24492  mulle0b  24493  fprodrecl  24580  iprodrecl  24609  rerisefaccl  24623  refallfaccl  24624  axcontlem2  25152  csbrn  25786  trirn  25787  isbnd2  25830  isbnd3  25831  equivbnd  25837  pellexlem5  26241  pell1234qrmulcl  26263  pellfundex  26294  rmspecsqrnq  26314  jm2.24nn  26369  jm2.17a  26370  jm2.17b  26371  jm2.17c  26372  acongrep  26390  acongeq  26393  jm3.1lem2  26434  mulltgt0  27016  fmul01  27033  fmuldfeqlem1  27035  fmuldfeq  27036  fmul01lt1lem1  27037  fmul01lt1lem2  27038  stoweidlem1  27073  stoweidlem3  27075  stoweidlem11  27083  stoweidlem13  27085  stoweidlem14  27086  stoweidlem16  27088  stoweidlem17  27089  stoweidlem22  27094  stoweidlem24  27096  stoweidlem25  27097  stoweidlem26  27098  stoweidlem34  27106  stoweidlem36  27108  stoweidlem42  27114  stoweidlem48  27120  stoweidlem49  27121  stoweidlem51  27123  stoweidlem59  27131  stoweidlem60  27132
This theorem was proved from axioms:  ax-mulrcl 8890
  Copyright terms: Public domain W3C validator