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

Theorem remulcl 10059
Description: Alias for ax-mulrcl 10037, for naming consistency with remulcli 10092. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
remulcl ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Proof of Theorem remulcl
StepHypRef Expression
1 ax-mulrcl 10037 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  (class class class)co 6690  cr 9973   · cmul 9979
This theorem was proved from axioms:  ax-mulrcl 10037
This theorem is referenced by:  1re  10077  remulcli  10092  remulcld  10108  axmulgt0  10150  00id  10249  mul02lem1  10250  recextlem2  10696  recex  10697  lemul1  10913  ltmul12a  10917  lemul12b  10918  mulgt1  10920  mulge0b  10931  mulle0b  10932  ltdivmul  10936  ledivmul  10937  lt2mul2div  10939  lemuldiv  10941  ltdiv23  10952  lediv23  10953  supmullem2  11032  cju  11054  addltmul  11306  zmulcl  11464  irrmul  11851  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  rpmulcl  11893  xmulasslem3  12154  xadddilem  12162  ge0mulcl  12323  iccdil  12348  mulmod0  12716  modmulnn  12728  modcyc  12745  modmul1  12763  modaddmulmod  12777  moddi  12778  addmodlteq  12785  reexpcl  12917  reexpclz  12920  expge0  12936  expge1  12937  expubnd  12961  bernneq  13030  expmulnbnd  13036  digit2  13037  digit1  13038  discr  13041  faclbnd  13117  faclbnd3  13119  faclbnd5  13125  facavg  13128  cshweqrep  13613  crre  13898  remim  13901  mulre  13905  sqrlem6  14032  sqrlem7  14033  sqreulem  14143  amgm2  14153  o1mul  14389  caucvgrlem  14447  climcndslem2  14626  climcnds  14627  fprodrecl  14727  fprodreclf  14733  iprodrecl  14777  rerisefaccl  14792  refallfaccl  14793  efcllem  14852  ege2le3  14864  ef01bndlem  14958  cos01gt0  14965  modprm0  15557  prmreclem3  15669  4sqlem11  15706  resubdrg  20002  nmoco  22588  nghmco  22589  blcvx  22648  iihalf1  22777  iihalf2  22779  iimulcl  22783  pcoass  22870  tchcphlem1  23080  csbren  23228  trirn  23229  minveclem2  23243  sca2rab  23326  uniioombllem5  23401  mbfmulc2lem  23459  i1fmul  23508  i1fmulclem  23514  i1fmulc  23515  dveflem  23787  cmvth  23799  dvivthlem1  23816  dvfsumle  23829  dvfsumlem2  23835  pilem2  24251  tangtx  24302  sinq12gt0  24304  coskpi  24317  cosne0  24321  efif1olem2  24334  efif1olem4  24336  relogexp  24387  logcxp  24460  rpcxpcl  24467  abscxpbnd  24539  ang180lem1  24584  atantan  24695  atanbndlem  24697  o1cxp  24746  divsqrtsumlem  24751  jensenlem2  24759  jensen  24760  zetacvg  24786  regamcl  24832  basellem1  24852  basellem4  24855  basellem9  24860  chtublem  24981  chtub  24982  logfaclbnd  24992  bpos1lem  25052  bposlem1  25054  bposlem2  25055  bposlem6  25059  bposlem7  25060  bposlem9  25062  lgseisen  25149  chebbnd1lem2  25204  chebbnd1lem3  25205  chto1ub  25210  rplogsumlem1  25218  dchrisumlem3  25225  dchrvmasumlem2  25232  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2  25252  mulog2sumlem1  25268  mulog2sumlem2  25269  log2sumbnd  25278  selberglem2  25280  chpdifbndlem1  25287  logdivbnd  25290  pntrlog2bndlem4  25314  pntibndlem2  25325  pntibndlem3  25326  pntlemh  25333  pntlemr  25336  pntlemk  25340  pntlemo  25341  ostth2lem1  25352  ostth2lem3  25369  ostth3  25372  axcontlem2  25890  nmoub3i  27756  blocni  27788  ubthlem3  27856  minvecolem2  27859  bcs2  28167  nmopub2tALT  28896  nmfnleub2  28913  nmophmi  29018  bdophmi  29019  lnconi  29020  cnlnadjlem2  29055  cnlnadjlem7  29060  nmopadjlem  29076  nmopcoadji  29088  leopnmid  29125  cdj1i  29420  cdj3lem2b  29424  cdj3i  29428  addltmulALT  29433  pnfinf  29865  rezh  30143  sgnmul  30732  sgnmulsgn  30739  sgnmulsgp  30740  signshf  30793  knoppndvlem15  32642  knoppndvlem21  32648  itg2addnclem  33591  ftc1anclem3  33617  isbnd2  33712  isbnd3  33713  equivbnd  33719  pellexlem5  37714  pell1234qrmulcl  37736  pellfundex  37767  rmspecsqrtnq  37787  rmspecsqrtnqOLD  37788  jm2.24nn  37843  jm2.17a  37844  jm2.17b  37845  jm2.17c  37846  acongrep  37864  acongeq  37867  jm3.1lem2  37902  mulltgt0  39495  ltdiv23neg  39930  fmul01  40130  fmuldfeq  40133  fmul01lt1lem1  40134  fmul01lt1lem2  40135  stoweidlem3  40538  stoweidlem13  40548  stoweidlem17  40552  stoweidlem34  40569  stoweidlem42  40577  stoweidlem48  40583  fourierdlem83  40724  hoidmvlelem2  41131  smfmullem1  41319  2leaddle2  41637  amgmwlem  42876
  Copyright terms: Public domain W3C validator