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

Theorem remulcl 8838
Description: Alias for ax-mulrcl 8816, for naming consistency with remulcli 8867. (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 8816 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 1696  (class class class)co 5874   RRcr 8752    x. cmul 8758
This theorem is referenced by:  1re  8853  remulcli  8867  remulcld  8879  axmulgt0  8913  00id  9003  mul02lem1  9004  recextlem2  9415  recex  9416  lemul1  9624  ltmul12a  9628  lemul12b  9629  mulgt1  9631  ltdivmul  9644  ledivmul  9645  ledivmulOLD  9646  lt2mul2div  9648  lemuldiv  9651  ltdiv23  9663  lediv23  9664  supmullem2  9737  cju  9758  addltmul  9963  zmulcl  10082  irrmul  10357  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem5  10362  rpmulcl  10391  xmulasslem3  10622  xadddilem  10630  ge0mulcl  10765  iccdil  10789  modmulnn  11004  modcyc  11015  modmul1  11018  moddi  11023  reexpcl  11136  reexpclz  11139  expge0  11154  expge1  11155  expubnd  11178  bernneq  11243  expmulnbnd  11249  digit2  11250  digit1  11251  discr  11254  faclbnd  11319  faclbnd3  11321  faclbnd5  11327  facavg  11330  crre  11615  remim  11618  mulre  11622  sqrlem6  11749  sqrlem7  11750  sqreulem  11859  amgm2  11869  o1mul  12104  caucvgrlem  12161  climcndslem2  12325  climcnds  12326  efcllem  12375  ege2le3  12387  ef01bndlem  12480  cos01gt0  12487  prmreclem3  12981  4sqlem11  13018  resubdrg  16439  nmoco  18262  nghmco  18263  blcvx  18320  iihalf1  18445  iihalf2  18447  iimulcl  18451  pcoass  18538  tchcphlem1  18681  minveclem2  18806  sca2rab  18887  uniioombllem5  18958  mbfmulc2lem  19018  i1fmul  19067  i1fmulclem  19073  i1fmulc  19074  dveflem  19342  cmvth  19354  dvivthlem1  19371  dvfsumle  19384  dvfsumlem2  19390  pilem2  19844  tangtx  19889  sinq12gt0  19891  coskpi  19904  cosne0  19908  efif1olem2  19921  efif1olem4  19923  relogexp  19965  logcxp  20032  rpcxpcl  20039  abscxpbnd  20109  ang180lem1  20123  atantan  20235  atanbndlem  20237  o1cxp  20285  divsqrsumlem  20290  jensenlem2  20298  jensen  20299  basellem1  20334  basellem4  20337  basellem9  20342  chtublem  20466  chtub  20467  logfaclbnd  20477  bpos1lem  20537  bposlem1  20539  bposlem2  20540  bposlem6  20544  bposlem7  20545  bposlem9  20547  lgseisen  20608  chebbnd1lem2  20635  chebbnd1lem3  20636  chto1ub  20641  rplogsumlem1  20649  dchrisumlem3  20656  dchrvmasumlem2  20663  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0lem2  20683  mulog2sumlem1  20699  mulog2sumlem2  20700  log2sumbnd  20709  selberglem2  20711  chpdifbndlem1  20718  logdivbnd  20721  pntrlog2bndlem4  20745  pntibndlem2  20756  pntibndlem3  20757  pntlemh  20764  pntlemr  20767  pntlemk  20771  pntlemo  20772  ostth2lem1  20783  ostth2lem3  20800  ostth3  20803  nmoub3i  21367  blocni  21399  ubthlem3  21467  minvecolem2  21470  bcs2  21777  nmopub2tALT  22505  nmfnleub2  22522  nmophmi  22627  bdophmi  22628  lnconi  22629  cnlnadjlem2  22664  cnlnadjlem7  22669  nmopadjlem  22685  nmopcoadji  22697  leopnmid  22734  cdj1i  23029  cdj3lem2b  23033  cdj3i  23037  addltmulALT  23042  zetacvg  23704  mulge0b  24101  mulle0b  24102  faclimlem5  24121  axcontlem2  24665  mslb1  25710  clsmulrv  25786  csbrn  26565  trirn  26566  isbnd2  26610  isbnd3  26611  equivbnd  26617  pellexlem5  27021  pell1234qrmulcl  27043  pellfundex  27074  rmspecsqrnq  27094  jm2.24nn  27149  jm2.17a  27150  jm2.17b  27151  jm2.17c  27152  acongrep  27170  acongeq  27173  jm3.1lem2  27214  mulltgt0  27796  fmul01  27813  fmuldfeqlem1  27815  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  stoweidlem1  27853  stoweidlem3  27855  stoweidlem11  27863  stoweidlem13  27865  stoweidlem14  27866  stoweidlem16  27868  stoweidlem17  27869  stoweidlem22  27874  stoweidlem24  27876  stoweidlem25  27877  stoweidlem26  27878  stoweidlem34  27886  stoweidlem36  27888  stoweidlem42  27894  stoweidlem48  27900  stoweidlem49  27901  stoweidlem51  27903  stoweidlem59  27911  stoweidlem60  27912
This theorem was proved from axioms:  ax-mulrcl 8816
  Copyright terms: Public domain W3C validator