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

Theorem remulcl 9077
Description: Alias for ax-mulrcl 9055, for naming consistency with remulcli 9106. (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 9055 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726  (class class class)co 6083   RRcr 8991    x. cmul 8997
This theorem is referenced by:  1re  9092  remulcli  9106  remulcld  9118  axmulgt0  9152  00id  9243  mul02lem1  9244  recextlem2  9655  recex  9656  lemul1  9864  ltmul12a  9868  lemul12b  9869  mulgt1  9871  ltdivmul  9884  ledivmul  9885  ledivmulOLD  9886  lt2mul2div  9888  lemuldiv  9891  ltdiv23  9903  lediv23  9904  supmullem2  9977  cju  9998  addltmul  10205  zmulcl  10326  irrmul  10601  rpnnen1lem1  10602  rpnnen1lem2  10603  rpnnen1lem3  10604  rpnnen1lem5  10606  rpmulcl  10635  xmulasslem3  10867  xadddilem  10875  ge0mulcl  11012  iccdil  11036  modmulnn  11267  modcyc  11278  modmul1  11281  moddi  11286  reexpcl  11400  reexpclz  11403  expge0  11418  expge1  11419  expubnd  11442  bernneq  11507  expmulnbnd  11513  digit2  11514  digit1  11515  discr  11518  faclbnd  11583  faclbnd3  11585  faclbnd5  11591  facavg  11594  crre  11921  remim  11924  mulre  11928  sqrlem6  12055  sqrlem7  12056  sqreulem  12165  amgm2  12175  o1mul  12410  caucvgrlem  12468  climcndslem2  12632  climcnds  12633  efcllem  12682  ege2le3  12694  ef01bndlem  12787  cos01gt0  12794  prmreclem3  13288  4sqlem11  13325  resubdrg  16752  nmoco  18773  nghmco  18774  blcvx  18831  iihalf1  18958  iihalf2  18960  iimulcl  18964  pcoass  19051  tchcphlem1  19194  minveclem2  19329  sca2rab  19410  uniioombllem5  19481  mbfmulc2lem  19541  i1fmul  19590  i1fmulclem  19596  i1fmulc  19597  dveflem  19865  cmvth  19877  dvivthlem1  19894  dvfsumle  19907  dvfsumlem2  19913  pilem2  20370  tangtx  20415  sinq12gt0  20417  coskpi  20430  cosne0  20434  efif1olem2  20447  efif1olem4  20449  relogexp  20492  logcxp  20562  rpcxpcl  20569  abscxpbnd  20639  ang180lem1  20653  atantan  20765  atanbndlem  20767  o1cxp  20815  divsqrsumlem  20820  jensenlem2  20828  jensen  20829  basellem1  20865  basellem4  20868  basellem9  20873  chtublem  20997  chtub  20998  logfaclbnd  21008  bpos1lem  21068  bposlem1  21070  bposlem2  21071  bposlem6  21075  bposlem7  21076  bposlem9  21078  lgseisen  21139  chebbnd1lem2  21166  chebbnd1lem3  21167  chto1ub  21172  rplogsumlem1  21180  dchrisumlem3  21187  dchrvmasumlem2  21194  dchrisum0lem1b  21211  dchrisum0lem1  21212  dchrisum0lem2  21214  mulog2sumlem1  21230  mulog2sumlem2  21231  log2sumbnd  21240  selberglem2  21242  chpdifbndlem1  21249  logdivbnd  21252  pntrlog2bndlem4  21276  pntibndlem2  21287  pntibndlem3  21288  pntlemh  21295  pntlemr  21298  pntlemk  21302  pntlemo  21303  ostth2lem1  21314  ostth2lem3  21331  ostth3  21334  nmoub3i  22276  blocni  22308  ubthlem3  22376  minvecolem2  22379  bcs2  22686  nmopub2tALT  23414  nmfnleub2  23431  nmophmi  23536  bdophmi  23537  lnconi  23538  cnlnadjlem2  23573  cnlnadjlem7  23578  nmopadjlem  23594  nmopcoadji  23606  leopnmid  23643  cdj1i  23938  cdj3lem2b  23942  cdj3i  23946  addltmulALT  23951  pnfinf  24255  rezh  24357  zetacvg  24801  regamcl  24847  mulge0b  25193  mulle0b  25194  fprodrecl  25281  iprodrecl  25317  rerisefaccl  25335  refallfaccl  25336  axcontlem2  25906  itg2addnclem  26258  ftc1anclem3  26284  csbrn  26458  trirn  26459  isbnd2  26494  isbnd3  26495  equivbnd  26501  pellexlem5  26898  pell1234qrmulcl  26920  pellfundex  26951  rmspecsqrnq  26971  jm2.24nn  27026  jm2.17a  27027  jm2.17b  27028  jm2.17c  27029  acongrep  27047  acongeq  27050  jm3.1lem2  27091  mulltgt0  27671  fmul01  27688  fmuldfeq  27691  fmul01lt1lem1  27692  fmul01lt1lem2  27693  stoweidlem3  27730  stoweidlem13  27740  stoweidlem17  27744  stoweidlem34  27761  stoweidlem42  27769  stoweidlem48  27775  2leaddle2  28103  modaddmulmod  28169  modidmul0  28171  modprm0  28250  cshweqrep  28296
This theorem was proved from axioms:  ax-mulrcl 9055
  Copyright terms: Public domain W3C validator