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

Theorem remulcl 8818
Description: Alias for ax-mulrcl 8796, for naming consistency with remulcli 8847. (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 8796 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 1685  (class class class)co 5820   RRcr 8732    x. cmul 8738
This theorem is referenced by:  1re  8833  remulcli  8847  remulcld  8859  axmulgt0  8893  00id  8983  mul02lem1  8984  recextlem2  9395  recex  9396  lemul1  9604  ltmul12a  9608  lemul12b  9609  mulgt1  9611  ltdivmul  9624  ledivmul  9625  ledivmulOLD  9626  lt2mul2div  9628  lemuldiv  9631  ltdiv23  9643  lediv23  9644  supmullem2  9717  cju  9738  addltmul  9943  zmulcl  10062  irrmul  10337  rpnnen1lem1  10338  rpnnen1lem2  10339  rpnnen1lem3  10340  rpnnen1lem5  10342  rpmulcl  10371  xmulasslem3  10602  xadddilem  10610  ge0mulcl  10745  iccdil  10769  modmulnn  10984  modcyc  10995  modmul1  10998  moddi  11003  reexpcl  11116  reexpclz  11119  expge0  11134  expge1  11135  expubnd  11158  bernneq  11223  expmulnbnd  11229  digit2  11230  digit1  11231  discr  11234  faclbnd  11299  faclbnd3  11301  faclbnd5  11307  facavg  11310  crre  11595  remim  11598  mulre  11602  sqrlem6  11729  sqrlem7  11730  sqreulem  11839  amgm2  11849  o1mul  12084  caucvgrlem  12141  climcndslem2  12305  climcnds  12306  efcllem  12355  ege2le3  12367  ef01bndlem  12460  cos01gt0  12467  prmreclem3  12961  4sqlem11  12998  resubdrg  16419  nmoco  18242  nghmco  18243  blcvx  18300  iihalf1  18425  iihalf2  18427  iimulcl  18431  pcoass  18518  tchcphlem1  18661  minveclem2  18786  sca2rab  18867  uniioombllem5  18938  mbfmulc2lem  18998  i1fmul  19047  i1fmulclem  19053  i1fmulc  19054  dveflem  19322  cmvth  19334  dvivthlem1  19351  dvfsumle  19364  dvfsumlem2  19370  pilem2  19824  tangtx  19869  sinq12gt0  19871  coskpi  19884  cosne0  19888  efif1olem2  19901  efif1olem4  19903  relogexp  19945  logcxp  20012  rpcxpcl  20019  abscxpbnd  20089  ang180lem1  20103  atantan  20215  atanbndlem  20217  o1cxp  20265  divsqrsumlem  20270  jensenlem2  20278  jensen  20279  basellem1  20314  basellem4  20317  basellem9  20322  chtublem  20446  chtub  20447  logfaclbnd  20457  bpos1lem  20517  bposlem1  20519  bposlem2  20520  bposlem6  20524  bposlem7  20525  bposlem9  20527  lgseisen  20588  chebbnd1lem2  20615  chebbnd1lem3  20616  chto1ub  20621  rplogsumlem1  20629  dchrisumlem3  20636  dchrvmasumlem2  20643  dchrisum0lem1b  20660  dchrisum0lem1  20661  dchrisum0lem2  20663  mulog2sumlem1  20679  mulog2sumlem2  20680  log2sumbnd  20689  selberglem2  20691  chpdifbndlem1  20698  logdivbnd  20701  pntrlog2bndlem4  20725  pntibndlem2  20736  pntibndlem3  20737  pntlemh  20744  pntlemr  20747  pntlemk  20751  pntlemo  20752  ostth2lem1  20763  ostth2lem3  20780  ostth3  20783  nmoub3i  21345  blocni  21377  ubthlem3  21445  minvecolem2  21448  bcs2  21757  nmopub2tALT  22485  nmfnleub2  22502  nmophmi  22607  bdophmi  22608  lnconi  22609  cnlnadjlem2  22644  cnlnadjlem7  22649  nmopadjlem  22665  nmopcoadji  22677  leopnmid  22714  cdj1i  23009  cdj3lem2b  23013  cdj3i  23017  addltmulALT  23022  zetacvg  23096  mulge0b  23492  mulle0b  23493  axcontlem2  24003  mslb1  25018  clsmulrv  25094  csbrn  25873  trirn  25874  isbnd2  25918  isbnd3  25919  equivbnd  25925  pellexlem5  26329  pell1234qrmulcl  26351  pellfundex  26382  rmspecsqrnq  26402  jm2.24nn  26457  jm2.17a  26458  jm2.17b  26459  jm2.17c  26460  acongrep  26478  acongeq  26481  jm3.1lem2  26522  mulltgt0  27104  fmul01  27121  fmuldfeqlem1  27123  fmuldfeq  27124  fmul01lt1lem1  27125  fmul01lt1lem2  27126  stoweidlem1  27161  stoweidlem3  27163  stoweidlem11  27171  stoweidlem13  27173  stoweidlem14  27174  stoweidlem16  27176  stoweidlem17  27177  stoweidlem22  27182  stoweidlem24  27184  stoweidlem25  27185  stoweidlem26  27186  stoweidlem34  27194  stoweidlem36  27196  stoweidlem42  27202  stoweidlem48  27208  stoweidlem49  27209  stoweidlem51  27211  stoweidlem59  27219  stoweidlem60  27220
This theorem was proved from axioms:  ax-mulrcl 8796
  Copyright terms: Public domain W3C validator