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

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

Proof of Theorem remulcl
StepHypRef Expression
1 ax-mulrcl 10593 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2112  (class class class)co 7139  cr 10529   · cmul 10535
This theorem was proved from axioms:  ax-mulrcl 10593
This theorem is referenced by:  1re  10634  remulcli  10650  remulcld  10664  axmulgt0  10708  00id  10808  mul02lem1  10809  recextlem2  11264  recex  11265  lemul1  11485  ltmul12a  11489  lemul12b  11490  mulgt1  11492  mulge0b  11503  mulle0b  11504  ltdivmul  11508  ledivmul  11509  lt2mul2div  11511  lemuldiv  11513  ltdiv23  11524  lediv23  11525  supmullem2  11603  cju  11625  addltmul  11865  zmulcl  12023  irrmul  12365  rpnnen1lem2  12368  rpnnen1lem1  12369  rpnnen1lem3  12370  rpnnen1lem5  12372  rpmulcl  12404  xmulasslem3  12671  xadddilem  12679  ge0mulcl  12843  iccdil  12872  mulmod0  13244  modmulnn  13256  modcyc  13273  modmul1  13291  modaddmulmod  13305  moddi  13306  addmodlteq  13313  reexpcl  13446  reexpclz  13449  expge0  13465  expge1  13466  expubnd  13541  bernneq  13590  expmulnbnd  13596  digit2  13597  digit1  13598  discr  13601  faclbnd  13650  faclbnd3  13652  faclbnd5  13658  facavg  13661  cshweqrep  14178  crre  14468  remim  14471  mulre  14475  sqrlem6  14602  sqrlem7  14603  sqreulem  14714  amgm2  14724  o1mul  14966  caucvgrlem  15024  climcndslem2  15200  climcnds  15201  fprodrecl  15302  fprodreclf  15308  iprodrecl  15351  rerisefaccl  15366  refallfaccl  15367  efcllem  15426  ege2le3  15438  ef01bndlem  15532  cos01gt0  15539  modprm0  16135  prmreclem3  16247  4sqlem11  16284  resubdrg  20300  nmoco  23346  nghmco  23347  blcvx  23406  iihalf1  23539  iihalf2  23541  iimulcl  23545  pcoass  23632  tcphcphlem1  23842  csbren  24006  trirn  24007  minveclem2  24033  sca2rab  24119  uniioombllem5  24194  mbfmulc2lem  24254  i1fmul  24303  i1fmulclem  24309  i1fmulc  24310  dveflem  24585  cmvth  24597  dvivthlem1  24614  dvfsumle  24627  dvfsumlem2  24633  pilem2  25050  tangtx  25101  sinq12gt0  25103  coskpi  25118  cosne0  25124  efif1olem2  25138  efif1olem4  25140  relogexp  25190  logcxp  25263  rpcxpcl  25270  abscxpbnd  25345  ang180lem1  25398  atantan  25512  atanbndlem  25514  o1cxp  25563  divsqrtsumlem  25568  jensenlem2  25576  jensen  25577  zetacvg  25603  regamcl  25649  basellem1  25669  basellem4  25672  basellem9  25677  chtublem  25798  chtub  25799  logfaclbnd  25809  bpos1lem  25869  bposlem1  25871  bposlem2  25872  bposlem6  25876  bposlem7  25877  bposlem9  25879  lgseisen  25966  chebbnd1lem2  26057  chebbnd1lem3  26058  chto1ub  26063  rplogsumlem1  26071  dchrisumlem3  26078  dchrvmasumlem2  26085  dchrisum0lem1b  26102  dchrisum0lem1  26103  dchrisum0lem2  26105  mulog2sumlem1  26121  mulog2sumlem2  26122  log2sumbnd  26131  selberglem2  26133  chpdifbndlem1  26140  logdivbnd  26143  pntrlog2bndlem4  26167  pntibndlem2  26178  pntibndlem3  26179  pntlemh  26186  pntlemr  26189  pntlemk  26193  pntlemo  26194  ostth2lem1  26205  ostth2lem3  26222  ostth3  26225  axcontlem2  26762  nmoub3i  28559  blocni  28591  ubthlem3  28658  minvecolem2  28661  bcs2  28968  nmopub2tALT  29695  nmfnleub2  29712  nmophmi  29817  bdophmi  29818  lnconi  29819  cnlnadjlem2  29854  cnlnadjlem7  29859  nmopadjlem  29875  nmopcoadji  29887  leopnmid  29924  cdj1i  30219  cdj3lem2b  30223  cdj3i  30227  addltmulALT  30232  pnfinf  30865  rezh  31320  sgnmul  31908  sgnmulsgn  31915  sgnmulsgp  31916  signshf  31966  knoppndvlem15  33973  knoppndvlem21  33979  itg2addnclem  35101  ftc1anclem3  35125  isbnd2  35214  isbnd3  35215  equivbnd  35221  2xp3dxp2ge1d  39374  resubdi  39521  pellexlem5  39761  pell1234qrmulcl  39783  pellfundex  39814  rmspecsqrtnq  39834  jm2.24nn  39887  jm2.17a  39888  jm2.17b  39889  jm2.17c  39890  acongrep  39908  acongeq  39911  jm3.1lem2  39946  mulltgt0  41638  ltdiv23neg  42017  fmul01  42209  fmuldfeq  42212  fmul01lt1lem1  42213  fmul01lt1lem2  42214  stoweidlem3  42632  stoweidlem13  42642  stoweidlem17  42646  stoweidlem34  42663  stoweidlem42  42671  stoweidlem48  42677  fourierdlem83  42818  hoidmvlelem2  43222  smfmullem1  43410  2leaddle2  43842  itsclc0lem1  45157  amgmwlem  45317
  Copyright terms: Public domain W3C validator