Theorem remulcl 11196

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

Assertion

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

Proof of Theorem remulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  (class class class)co 7416  ℝcr 11110   · cmul 11116

This proof depends on axioms:  ax-mulrcl 11174

This theorem is used by:  1re  11219  remulcli  11236  remulcld  11250  axmulgt0  11295  00id  11396  mul02lem1  11397  recextlem2  11856  recex  11857  lemul1  12078  ltmul12a  12082  lemul12b  12083  mulgt1  12087  mulge0b  12096  mulle0b  12097  ltdivmul  12101  ledivmul  12102  lt2mul2div  12104  lemuldiv  12106  ltdiv23  12117  lediv23  12118  supmullem2  12197  cju  12225  addltmul  12491  zmulcl  12654  irrmul  13010  rpnnen1lem2  13013  rpnnen1lem1  13014  rpnnen1lem3  13015  rpnnen1lem5  13017  rpmulcl  13053  xmulasslem3  13324  xadddilem  13332  ge0mulcl  13500  iccdil  13529  mulmod0  13924  modmulnn  13936  modcyc  13953  modmul1  13974  modaddmulmod  13988  moddi  13989  addmodlteq  13996  reexpcl  14128  reexpclz  14132  expge0  14148  expge1  14149  expubnd  14228  bernneq  14279  expmulnbnd  14285  digit2  14286  digit1  14287  discr  14290  faclbnd  14340  faclbnd3  14342  faclbnd5  14348  facavg  14351  cshweqrep  14878  sgnmul  15164  sgnmulsgn  15166  crre  15185  remim  15188  mulre  15192  01sqrexlem6  15318  01sqrexlem7  15319  sqreulem  15431  amgm2  15441  o1mul  15686  caucvgrlem  15744  climcndslem2  15923  climcnds  15924  fprodrecl  16026  fprodreclf  16032  iprodrecl  16075  rerisefaccl  16090  refallfaccl  16091  efcllem  16149  ege2le3  16162  ef01bndlem  16258  cos01gt0  16265  modprm0  16883  prmreclem3  16996  4sqlem11  17033  resubdrg  21788  nmoco  24925  nghmco  24926  blcvx  24986  iihalf1  25121  iihalf2  25123  iimulcl  25127  pcoass  25214  tcphcphlem1  25425  csbren  25589  trirn  25590  minveclem2  25616  sca2rab  25702  uniioombllem5  25777  mbfmulc2lem  25837  i1fmul  25886  i1fmulclem  25892  i1fmulc  25893  dveflem  26169  cmvth  26181  dvivthlem1  26198  dvfsumle  26211  dvfsumlem2  26217  pilem2  26646  tangtx  26701  sinq12gt0  26703  coskpi  26719  cosne0  26725  efif1olem2  26739  efif1olem4  26741  relogexp  26792  logcxp  26865  rpcxpcl  26872  abscxpbnd  26949  ang180lem1  27005  atantan  27119  atanbndlem  27121  o1cxp  27170  divsqrtsumlem  27175  jensenlem2  27183  jensen  27184  zetacvg  27210  regamcl  27256  basellem1  27276  basellem4  27279  basellem9  27284  chtublem  27406  chtub  27407  logfaclbnd  27417  bpos1lem  27477  bposlem1  27479  bposlem2  27480  bposlem6  27484  bposlem7  27485  bposlem9  27487  lgseisen  27574  chebbnd1lem2  27665  chebbnd1lem3  27666  chto1ub  27671  rplogsumlem1  27679  dchrisumlem3  27686  dchrvmasumlem2  27693  dchrisum0lem1b  27710  dchrisum0lem1  27711  dchrisum0lem2  27713  mulog2sumlem1  27729  mulog2sumlem2  27730  log2sumbnd  27739  selberglem2  27741  chpdifbndlem1  27748  logdivbnd  27751  pntrlog2bndlem4  27775  pntibndlem2  27786  pntibndlem3  27787  pntlemh  27794  pntlemr  27797  pntlemk  27801  pntlemo  27802  ostth2lem1  27813  ostth2lem3  27830  ostth3  27833  axcontlem2  29346  nmoub3i  31172  blocni  31204  ubthlem3  31271  minvecolem2  31274  bcs2  31581  nmopub2tALT  32308  nmfnleub2  32325  nmophmi  32430  bdophmi  32431  lnconi  32432  cnlnadjlem2  32467  cnlnadjlem7  32472  nmopadjlem  32488  nmopcoadji  32500  leopnmid  32537  cdj1i  32832  cdj3lem2b  32836  cdj3i  32840  addltmulALT  32845  sgnmulsgp  33222  pnfinf  33543  rezh  34399  signshf  35016  knoppndvlem15  37148  knoppndvlem21  37154  itg2addnclem  38355  ftc1anclem3  38379  isbnd2  38467  isbnd3  38468  equivbnd  38474  aks6d1c7lem1  42980  resubdi  43190  pellexlem5  43593  pell1234qrmulcl  43615  pellfundex  43646  rmspecsqrtnq  43666  jm2.24nn  43719  jm2.17a  43720  jm2.17b  43721  jm2.17c  43722  acongrep  43740  acongeq  43743  jm3.1lem2  43778  mulltgt0  45775  ltdiv23neg  46142  fmul01  46329  fmuldfeq  46332  fmul01lt1lem1  46333  fmul01lt1lem2  46334  stoweidlem3  46750  stoweidlem13  46760  stoweidlem17  46764  stoweidlem34  46781  stoweidlem42  46789  stoweidlem48  46795  fourierdlem83  46936  hoidmvlelem2  47343  smfmullem1  47538  2leaddle2  48068  itsclc0lem1  49569  crosspalti  50681  amgmwlem  50683