Theorem remulcl 11114

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  (class class class)co 7356  ℝcr 11028   · cmul 11034

This theorem was proved from axioms:  ax-mulrcl 11092

This theorem is referenced by:  1re  11135  remulcli  11152  remulcld  11166  axmulgt0  11211  00id  11312  mul02lem1  11313  recextlem2  11772  recex  11773  lemul1  11998  ltmul12a  12002  lemul12b  12003  mulgt1OLD  12005  mulgt1  12008  mulge0b  12017  mulle0b  12018  ltdivmul  12022  ledivmul  12023  lt2mul2div  12025  lemuldiv  12027  ltdiv23  12038  lediv23  12039  supmullem2  12118  cju  12146  addltmul  12404  zmulcl  12567  irrmul  12915  rpnnen1lem2  12918  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  rpmulcl  12958  xmulasslem3  13229  xadddilem  13237  ge0mulcl  13405  iccdil  13434  mulmod0  13827  modmulnn  13839  modcyc  13856  modmul1  13877  modaddmulmod  13891  moddi  13892  addmodlteq  13899  reexpcl  14031  reexpclz  14035  expge0  14051  expge1  14052  expubnd  14131  bernneq  14182  expmulnbnd  14188  digit2  14189  digit1  14190  discr  14193  faclbnd  14243  faclbnd3  14245  faclbnd5  14251  facavg  14254  cshweqrep  14774  crre  15067  remim  15070  mulre  15074  01sqrexlem6  15200  01sqrexlem7  15201  sqreulem  15313  amgm2  15323  o1mul  15568  caucvgrlem  15626  climcndslem2  15806  climcnds  15807  fprodrecl  15909  fprodreclf  15915  iprodrecl  15958  rerisefaccl  15973  refallfaccl  15974  efcllem  16033  ege2le3  16046  ef01bndlem  16142  cos01gt0  16149  modprm0  16767  prmreclem3  16880  4sqlem11  16917  resubdrg  21583  nmoco  24720  nghmco  24721  blcvx  24781  iihalf1  24916  iihalf2  24918  iimulcl  24922  pcoass  25009  tcphcphlem1  25220  csbren  25384  trirn  25385  minveclem2  25411  sca2rab  25497  uniioombllem5  25572  mbfmulc2lem  25632  i1fmul  25681  i1fmulclem  25687  i1fmulc  25688  dveflem  25964  cmvth  25976  dvivthlem1  25993  dvfsumle  26006  dvfsumlem2  26012  pilem2  26435  tangtx  26487  sinq12gt0  26489  coskpi  26505  cosne0  26511  efif1olem2  26525  efif1olem4  26527  relogexp  26578  logcxp  26651  rpcxpcl  26658  abscxpbnd  26735  ang180lem1  26791  atantan  26905  atanbndlem  26907  o1cxp  26956  divsqrtsumlem  26961  jensenlem2  26969  jensen  26970  zetacvg  26996  regamcl  27042  basellem1  27062  basellem4  27065  basellem9  27070  chtublem  27192  chtub  27193  logfaclbnd  27203  bpos1lem  27263  bposlem1  27265  bposlem2  27266  bposlem6  27270  bposlem7  27271  bposlem9  27273  lgseisen  27360  chebbnd1lem2  27451  chebbnd1lem3  27452  chto1ub  27457  rplogsumlem1  27465  dchrisumlem3  27472  dchrvmasumlem2  27479  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2  27499  mulog2sumlem1  27515  mulog2sumlem2  27516  log2sumbnd  27525  selberglem2  27527  chpdifbndlem1  27534  logdivbnd  27537  pntrlog2bndlem4  27561  pntibndlem2  27572  pntibndlem3  27573  pntlemh  27580  pntlemr  27583  pntlemk  27587  pntlemo  27588  ostth2lem1  27599  ostth2lem3  27616  ostth3  27619  axcontlem2  29052  nmoub3i  30862  blocni  30894  ubthlem3  30961  minvecolem2  30964  bcs2  31271  nmopub2tALT  31998  nmfnleub2  32015  nmophmi  32120  bdophmi  32121  lnconi  32122  cnlnadjlem2  32157  cnlnadjlem7  32162  nmopadjlem  32178  nmopcoadji  32190  leopnmid  32227  cdj1i  32522  cdj3lem2b  32526  cdj3i  32530  addltmulALT  32535  sgnmul  32927  sgnmulsgn  32934  sgnmulsgp  32935  pnfinf  33264  rezh  34153  signshf  34772  knoppndvlem15  36832  knoppndvlem21  36838  itg2addnclem  38038  ftc1anclem3  38062  isbnd2  38150  isbnd3  38151  equivbnd  38157  aks6d1c7lem1  42665  resubdi  42873  pellexlem5  43278  pell1234qrmulcl  43300  pellfundex  43331  rmspecsqrtnq  43351  jm2.24nn  43404  jm2.17a  43405  jm2.17b  43406  jm2.17c  43407  acongrep  43425  acongeq  43428  jm3.1lem2  43463  mulltgt0  45470  ltdiv23neg  45838  fmul01  46025  fmuldfeq  46028  fmul01lt1lem1  46029  fmul01lt1lem2  46030  stoweidlem3  46446  stoweidlem13  46456  stoweidlem17  46460  stoweidlem34  46477  stoweidlem42  46485  stoweidlem48  46491  fourierdlem83  46632  hoidmvlelem2  47039  smfmullem1  47234  2leaddle2  47761  itsclc0lem1  49247  amgmwlem  50292