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

Theorem remulcl 8822
Description: Alias for ax-mulrcl 8800, for naming consistency with remulcli 8851. (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 8800 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 1684  (class class class)co 5858   RRcr 8736    x. cmul 8742
This theorem is referenced by:  1re  8837  remulcli  8851  remulcld  8863  axmulgt0  8897  00id  8987  mul02lem1  8988  recextlem2  9399  recex  9400  lemul1  9608  ltmul12a  9612  lemul12b  9613  mulgt1  9615  ltdivmul  9628  ledivmul  9629  ledivmulOLD  9630  lt2mul2div  9632  lemuldiv  9635  ltdiv23  9647  lediv23  9648  supmullem2  9721  cju  9742  addltmul  9947  zmulcl  10066  irrmul  10341  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  rpmulcl  10375  xmulasslem3  10606  xadddilem  10614  ge0mulcl  10749  iccdil  10773  modmulnn  10988  modcyc  10999  modmul1  11002  moddi  11007  reexpcl  11120  reexpclz  11123  expge0  11138  expge1  11139  expubnd  11162  bernneq  11227  expmulnbnd  11233  digit2  11234  digit1  11235  discr  11238  faclbnd  11303  faclbnd3  11305  faclbnd5  11311  facavg  11314  crre  11599  remim  11602  mulre  11606  sqrlem6  11733  sqrlem7  11734  sqreulem  11843  amgm2  11853  o1mul  12088  caucvgrlem  12145  climcndslem2  12309  climcnds  12310  efcllem  12359  ege2le3  12371  ef01bndlem  12464  cos01gt0  12471  prmreclem3  12965  4sqlem11  13002  resubdrg  16423  nmoco  18246  nghmco  18247  blcvx  18304  iihalf1  18429  iihalf2  18431  iimulcl  18435  pcoass  18522  tchcphlem1  18665  minveclem2  18790  sca2rab  18871  uniioombllem5  18942  mbfmulc2lem  19002  i1fmul  19051  i1fmulclem  19057  i1fmulc  19058  dveflem  19326  cmvth  19338  dvivthlem1  19355  dvfsumle  19368  dvfsumlem2  19374  pilem2  19828  tangtx  19873  sinq12gt0  19875  coskpi  19888  cosne0  19892  efif1olem2  19905  efif1olem4  19907  relogexp  19949  logcxp  20016  rpcxpcl  20023  abscxpbnd  20093  ang180lem1  20107  atantan  20219  atanbndlem  20221  o1cxp  20269  divsqrsumlem  20274  jensenlem2  20282  jensen  20283  basellem1  20318  basellem4  20321  basellem9  20326  chtublem  20450  chtub  20451  logfaclbnd  20461  bpos1lem  20521  bposlem1  20523  bposlem2  20524  bposlem6  20528  bposlem7  20529  bposlem9  20531  lgseisen  20592  chebbnd1lem2  20619  chebbnd1lem3  20620  chto1ub  20625  rplogsumlem1  20633  dchrisumlem3  20640  dchrvmasumlem2  20647  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2  20667  mulog2sumlem1  20683  mulog2sumlem2  20684  log2sumbnd  20693  selberglem2  20695  chpdifbndlem1  20702  logdivbnd  20705  pntrlog2bndlem4  20729  pntibndlem2  20740  pntibndlem3  20741  pntlemh  20748  pntlemr  20751  pntlemk  20755  pntlemo  20756  ostth2lem1  20767  ostth2lem3  20784  ostth3  20787  nmoub3i  21351  blocni  21383  ubthlem3  21451  minvecolem2  21454  bcs2  21761  nmopub2tALT  22489  nmfnleub2  22506  nmophmi  22611  bdophmi  22612  lnconi  22613  cnlnadjlem2  22648  cnlnadjlem7  22653  nmopadjlem  22669  nmopcoadji  22681  leopnmid  22718  cdj1i  23013  cdj3lem2b  23017  cdj3i  23021  addltmulALT  23026  zetacvg  23689  mulge0b  24086  mulle0b  24087  axcontlem2  24593  mslb1  25607  clsmulrv  25683  csbrn  26462  trirn  26463  isbnd2  26507  isbnd3  26508  equivbnd  26514  pellexlem5  26918  pell1234qrmulcl  26940  pellfundex  26971  rmspecsqrnq  26991  jm2.24nn  27046  jm2.17a  27047  jm2.17b  27048  jm2.17c  27049  acongrep  27067  acongeq  27070  jm3.1lem2  27111  mulltgt0  27693  fmul01  27710  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  stoweidlem1  27750  stoweidlem3  27752  stoweidlem11  27760  stoweidlem13  27762  stoweidlem14  27763  stoweidlem16  27765  stoweidlem17  27766  stoweidlem22  27771  stoweidlem24  27773  stoweidlem25  27774  stoweidlem26  27775  stoweidlem34  27783  stoweidlem36  27785  stoweidlem42  27791  stoweidlem48  27797  stoweidlem49  27798  stoweidlem51  27800  stoweidlem59  27808  stoweidlem60  27809
This theorem was proved from axioms:  ax-mulrcl 8800
  Copyright terms: Public domain W3C validator