Theorem remulcl 11002

Description: Alias for ax-mulrcl 10980, for naming consistency with remulcli 11037. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
remulcl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Proof of Theorem remulcl

Step	Hyp	Ref	Expression
1		ax-mulrcl 10980	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2104  (class class class)co 7307  ℝcr 10916   · cmul 10922

This theorem was proved from axioms:  ax-mulrcl 10980

This theorem is referenced by:  1re  11021  remulcli  11037  remulcld  11051  axmulgt0  11095  00id  11196  mul02lem1  11197  recextlem2  11652  recex  11653  lemul1  11873  ltmul12a  11877  lemul12b  11878  mulgt1  11880  mulge0b  11891  mulle0b  11892  ltdivmul  11896  ledivmul  11897  lt2mul2div  11899  lemuldiv  11901  ltdiv23  11912  lediv23  11913  supmullem2  11992  cju  12015  addltmul  12255  zmulcl  12415  irrmul  12760  rpnnen1lem2  12763  rpnnen1lem1  12764  rpnnen1lem3  12765  rpnnen1lem5  12767  rpmulcl  12799  xmulasslem3  13066  xadddilem  13074  ge0mulcl  13239  iccdil  13268  mulmod0  13643  modmulnn  13655  modcyc  13672  modmul1  13690  modaddmulmod  13704  moddi  13705  addmodlteq  13712  reexpcl  13845  reexpclz  13848  expge0  13865  expge1  13866  expubnd  13941  bernneq  13990  expmulnbnd  13996  digit2  13997  digit1  13998  discr  14001  faclbnd  14050  faclbnd3  14052  faclbnd5  14058  facavg  14061  cshweqrep  14579  crre  14870  remim  14873  mulre  14877  sqrlem6  15004  sqrlem7  15005  sqreulem  15116  amgm2  15126  o1mul  15369  caucvgrlem  15429  climcndslem2  15607  climcnds  15608  fprodrecl  15708  fprodreclf  15714  iprodrecl  15757  rerisefaccl  15772  refallfaccl  15773  efcllem  15832  ege2le3  15844  ef01bndlem  15938  cos01gt0  15945  modprm0  16551  prmreclem3  16664  4sqlem11  16701  resubdrg  20858  nmoco  23946  nghmco  23947  blcvx  24006  iihalf1  24139  iihalf2  24141  iimulcl  24145  pcoass  24232  tcphcphlem1  24444  csbren  24608  trirn  24609  minveclem2  24635  sca2rab  24721  uniioombllem5  24796  mbfmulc2lem  24856  i1fmul  24905  i1fmulclem  24912  i1fmulc  24913  dveflem  25188  cmvth  25200  dvivthlem1  25217  dvfsumle  25230  dvfsumlem2  25236  pilem2  25656  tangtx  25707  sinq12gt0  25709  coskpi  25724  cosne0  25730  efif1olem2  25744  efif1olem4  25746  relogexp  25796  logcxp  25869  rpcxpcl  25876  abscxpbnd  25951  ang180lem1  26004  atantan  26118  atanbndlem  26120  o1cxp  26169  divsqrtsumlem  26174  jensenlem2  26182  jensen  26183  zetacvg  26209  regamcl  26255  basellem1  26275  basellem4  26278  basellem9  26283  chtublem  26404  chtub  26405  logfaclbnd  26415  bpos1lem  26475  bposlem1  26477  bposlem2  26478  bposlem6  26482  bposlem7  26483  bposlem9  26485  lgseisen  26572  chebbnd1lem2  26663  chebbnd1lem3  26664  chto1ub  26669  rplogsumlem1  26677  dchrisumlem3  26684  dchrvmasumlem2  26691  dchrisum0lem1b  26708  dchrisum0lem1  26709  dchrisum0lem2  26711  mulog2sumlem1  26727  mulog2sumlem2  26728  log2sumbnd  26737  selberglem2  26739  chpdifbndlem1  26746  logdivbnd  26749  pntrlog2bndlem4  26773  pntibndlem2  26784  pntibndlem3  26785  pntlemh  26792  pntlemr  26795  pntlemk  26799  pntlemo  26800  ostth2lem1  26811  ostth2lem3  26828  ostth3  26831  axcontlem2  27378  nmoub3i  29180  blocni  29212  ubthlem3  29279  minvecolem2  29282  bcs2  29589  nmopub2tALT  30316  nmfnleub2  30333  nmophmi  30438  bdophmi  30439  lnconi  30440  cnlnadjlem2  30475  cnlnadjlem7  30480  nmopadjlem  30496  nmopcoadji  30508  leopnmid  30545  cdj1i  30840  cdj3lem2b  30844  cdj3i  30848  addltmulALT  30853  pnfinf  31482  rezh  31966  sgnmul  32554  sgnmulsgn  32561  sgnmulsgp  32562  signshf  32612  knoppndvlem15  34751  knoppndvlem21  34757  itg2addnclem  35872  ftc1anclem3  35896  isbnd2  35985  isbnd3  35986  equivbnd  35992  2xp3dxp2ge1d  40204  resubdi  40416  pellexlem5  40692  pell1234qrmulcl  40714  pellfundex  40745  rmspecsqrtnq  40765  jm2.24nn  40819  jm2.17a  40820  jm2.17b  40821  jm2.17c  40822  acongrep  40840  acongeq  40843  jm3.1lem2  40878  mulltgt0  42603  ltdiv23neg  42982  fmul01  43170  fmuldfeq  43173  fmul01lt1lem1  43174  fmul01lt1lem2  43175  stoweidlem3  43593  stoweidlem13  43603  stoweidlem17  43607  stoweidlem34  43624  stoweidlem42  43632  stoweidlem48  43638  fourierdlem83  43779  hoidmvlelem2  44184  smfmullem1  44379  2leaddle2  44848  itsclc0lem1  46160  amgmwlem  46564