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

Theorem remulcl 9064
Description: Alias for ax-mulrcl 9042, for naming consistency with remulcli 9093. (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 9042 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725  (class class class)co 6072   RRcr 8978    x. cmul 8984
This theorem is referenced by:  1re  9079  remulcli  9093  remulcld  9105  axmulgt0  9139  00id  9230  mul02lem1  9231  recextlem2  9642  recex  9643  lemul1  9851  ltmul12a  9855  lemul12b  9856  mulgt1  9858  ltdivmul  9871  ledivmul  9872  ledivmulOLD  9873  lt2mul2div  9875  lemuldiv  9878  ltdiv23  9890  lediv23  9891  supmullem2  9964  cju  9985  addltmul  10192  zmulcl  10313  irrmul  10588  rpnnen1lem1  10589  rpnnen1lem2  10590  rpnnen1lem3  10591  rpnnen1lem5  10593  rpmulcl  10622  xmulasslem3  10854  xadddilem  10862  ge0mulcl  10999  iccdil  11023  modmulnn  11253  modcyc  11264  modmul1  11267  moddi  11272  reexpcl  11386  reexpclz  11389  expge0  11404  expge1  11405  expubnd  11428  bernneq  11493  expmulnbnd  11499  digit2  11500  digit1  11501  discr  11504  faclbnd  11569  faclbnd3  11571  faclbnd5  11577  facavg  11580  crre  11907  remim  11910  mulre  11914  sqrlem6  12041  sqrlem7  12042  sqreulem  12151  amgm2  12161  o1mul  12396  caucvgrlem  12454  climcndslem2  12618  climcnds  12619  efcllem  12668  ege2le3  12680  ef01bndlem  12773  cos01gt0  12780  prmreclem3  13274  4sqlem11  13311  resubdrg  16738  nmoco  18759  nghmco  18760  blcvx  18817  iihalf1  18944  iihalf2  18946  iimulcl  18950  pcoass  19037  tchcphlem1  19180  minveclem2  19315  sca2rab  19396  uniioombllem5  19467  mbfmulc2lem  19527  i1fmul  19576  i1fmulclem  19582  i1fmulc  19583  dveflem  19851  cmvth  19863  dvivthlem1  19880  dvfsumle  19893  dvfsumlem2  19899  pilem2  20356  tangtx  20401  sinq12gt0  20403  coskpi  20416  cosne0  20420  efif1olem2  20433  efif1olem4  20435  relogexp  20478  logcxp  20548  rpcxpcl  20555  abscxpbnd  20625  ang180lem1  20639  atantan  20751  atanbndlem  20753  o1cxp  20801  divsqrsumlem  20806  jensenlem2  20814  jensen  20815  basellem1  20851  basellem4  20854  basellem9  20859  chtublem  20983  chtub  20984  logfaclbnd  20994  bpos1lem  21054  bposlem1  21056  bposlem2  21057  bposlem6  21061  bposlem7  21062  bposlem9  21064  lgseisen  21125  chebbnd1lem2  21152  chebbnd1lem3  21153  chto1ub  21158  rplogsumlem1  21166  dchrisumlem3  21173  dchrvmasumlem2  21180  dchrisum0lem1b  21197  dchrisum0lem1  21198  dchrisum0lem2  21200  mulog2sumlem1  21216  mulog2sumlem2  21217  log2sumbnd  21226  selberglem2  21228  chpdifbndlem1  21235  logdivbnd  21238  pntrlog2bndlem4  21262  pntibndlem2  21273  pntibndlem3  21274  pntlemh  21281  pntlemr  21284  pntlemk  21288  pntlemo  21289  ostth2lem1  21300  ostth2lem3  21317  ostth3  21320  nmoub3i  22262  blocni  22294  ubthlem3  22362  minvecolem2  22365  bcs2  22672  nmopub2tALT  23400  nmfnleub2  23417  nmophmi  23522  bdophmi  23523  lnconi  23524  cnlnadjlem2  23559  cnlnadjlem7  23564  nmopadjlem  23580  nmopcoadji  23592  leopnmid  23629  cdj1i  23924  cdj3lem2b  23928  cdj3i  23932  addltmulALT  23937  pnfinf  24241  rezh  24343  zetacvg  24787  regamcl  24833  mulge0b  25179  mulle0b  25180  fprodrecl  25268  iprodrecl  25304  rerisefaccl  25322  refallfaccl  25323  axcontlem2  25852  itg2addnclem  26202  csbrn  26393  trirn  26394  isbnd2  26429  isbnd3  26430  equivbnd  26436  pellexlem5  26833  pell1234qrmulcl  26855  pellfundex  26886  rmspecsqrnq  26906  jm2.24nn  26961  jm2.17a  26962  jm2.17b  26963  jm2.17c  26964  acongrep  26982  acongeq  26985  jm3.1lem2  27026  mulltgt0  27607  fmul01  27624  fmuldfeq  27627  fmul01lt1lem1  27628  fmul01lt1lem2  27629  stoweidlem3  27666  stoweidlem13  27676  stoweidlem17  27680  stoweidlem34  27697  stoweidlem42  27705  stoweidlem48  27711  modaddmulmod  28064  modidmul0  28066  modprm0  28112  shwrdeqrep  28160
This theorem was proved from axioms:  ax-mulrcl 9042
  Copyright terms: Public domain W3C validator