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

Theorem remulcl 8824
Description: Alias for ax-mulrcl 8802, for naming consistency with remulcli 8853. (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 8802 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 1686  (class class class)co 5860   RRcr 8738    x. cmul 8744
This theorem is referenced by:  1re  8839  remulcli  8853  remulcld  8865  axmulgt0  8899  00id  8989  mul02lem1  8990  recextlem2  9401  recex  9402  lemul1  9610  ltmul12a  9614  lemul12b  9615  mulgt1  9617  ltdivmul  9630  ledivmul  9631  ledivmulOLD  9632  lt2mul2div  9634  lemuldiv  9637  ltdiv23  9649  lediv23  9650  supmullem2  9723  cju  9744  addltmul  9949  zmulcl  10068  irrmul  10343  rpnnen1lem1  10344  rpnnen1lem2  10345  rpnnen1lem3  10346  rpnnen1lem5  10348  rpmulcl  10377  xmulasslem3  10608  xadddilem  10616  ge0mulcl  10751  iccdil  10775  modmulnn  10990  modcyc  11001  modmul1  11004  moddi  11009  reexpcl  11122  reexpclz  11125  expge0  11140  expge1  11141  expubnd  11164  bernneq  11229  expmulnbnd  11235  digit2  11236  digit1  11237  discr  11240  faclbnd  11305  faclbnd3  11307  faclbnd5  11313  facavg  11316  crre  11601  remim  11604  mulre  11608  sqrlem6  11735  sqrlem7  11736  sqreulem  11845  amgm2  11855  o1mul  12090  caucvgrlem  12147  climcndslem2  12311  climcnds  12312  efcllem  12361  ege2le3  12373  ef01bndlem  12466  cos01gt0  12473  prmreclem3  12967  4sqlem11  13004  resubdrg  16425  nmoco  18248  nghmco  18249  blcvx  18306  iihalf1  18431  iihalf2  18433  iimulcl  18437  pcoass  18524  tchcphlem1  18667  minveclem2  18792  sca2rab  18873  uniioombllem5  18944  mbfmulc2lem  19004  i1fmul  19053  i1fmulclem  19059  i1fmulc  19060  dveflem  19328  cmvth  19340  dvivthlem1  19357  dvfsumle  19370  dvfsumlem2  19376  pilem2  19830  tangtx  19875  sinq12gt0  19877  coskpi  19890  cosne0  19894  efif1olem2  19907  efif1olem4  19909  relogexp  19951  logcxp  20018  rpcxpcl  20025  abscxpbnd  20095  ang180lem1  20109  atantan  20221  atanbndlem  20223  o1cxp  20271  divsqrsumlem  20276  jensenlem2  20284  jensen  20285  basellem1  20320  basellem4  20323  basellem9  20328  chtublem  20452  chtub  20453  logfaclbnd  20463  bpos1lem  20523  bposlem1  20525  bposlem2  20526  bposlem6  20530  bposlem7  20531  bposlem9  20533  lgseisen  20594  chebbnd1lem2  20621  chebbnd1lem3  20622  chto1ub  20627  rplogsumlem1  20635  dchrisumlem3  20642  dchrvmasumlem2  20649  dchrisum0lem1b  20666  dchrisum0lem1  20667  dchrisum0lem2  20669  mulog2sumlem1  20685  mulog2sumlem2  20686  log2sumbnd  20695  selberglem2  20697  chpdifbndlem1  20704  logdivbnd  20707  pntrlog2bndlem4  20731  pntibndlem2  20742  pntibndlem3  20743  pntlemh  20750  pntlemr  20753  pntlemk  20757  pntlemo  20758  ostth2lem1  20769  ostth2lem3  20786  ostth3  20789  nmoub3i  21353  blocni  21385  ubthlem3  21453  minvecolem2  21456  bcs2  21763  nmopub2tALT  22491  nmfnleub2  22508  nmophmi  22613  bdophmi  22614  lnconi  22615  cnlnadjlem2  22650  cnlnadjlem7  22655  nmopadjlem  22671  nmopcoadji  22683  leopnmid  22720  cdj1i  23015  cdj3lem2b  23019  cdj3i  23023  addltmulALT  23028  zetacvg  23691  mulge0b  24088  mulle0b  24089  axcontlem2  24595  mslb1  25618  clsmulrv  25694  csbrn  26473  trirn  26474  isbnd2  26518  isbnd3  26519  equivbnd  26525  pellexlem5  26929  pell1234qrmulcl  26951  pellfundex  26982  rmspecsqrnq  27002  jm2.24nn  27057  jm2.17a  27058  jm2.17b  27059  jm2.17c  27060  acongrep  27078  acongeq  27081  jm3.1lem2  27122  mulltgt0  27704  fmul01  27721  fmuldfeqlem1  27723  fmuldfeq  27724  fmul01lt1lem1  27725  fmul01lt1lem2  27726  stoweidlem1  27761  stoweidlem3  27763  stoweidlem11  27771  stoweidlem13  27773  stoweidlem14  27774  stoweidlem16  27776  stoweidlem17  27777  stoweidlem22  27782  stoweidlem24  27784  stoweidlem25  27785  stoweidlem26  27786  stoweidlem34  27794  stoweidlem36  27796  stoweidlem42  27802  stoweidlem48  27808  stoweidlem49  27809  stoweidlem51  27811  stoweidlem59  27819  stoweidlem60  27820
This theorem was proved from axioms:  ax-mulrcl 8802
  Copyright terms: Public domain W3C validator