Theorem remulcl 10940

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7268  ℝcr 10854   · cmul 10860

This theorem was proved from axioms:  ax-mulrcl 10918

This theorem is referenced by:  1re  10959  remulcli  10975  remulcld  10989  axmulgt0  11033  00id  11133  mul02lem1  11134  recextlem2  11589  recex  11590  lemul1  11810  ltmul12a  11814  lemul12b  11815  mulgt1  11817  mulge0b  11828  mulle0b  11829  ltdivmul  11833  ledivmul  11834  lt2mul2div  11836  lemuldiv  11838  ltdiv23  11849  lediv23  11850  supmullem2  11929  cju  11952  addltmul  12192  zmulcl  12352  irrmul  12696  rpnnen1lem2  12699  rpnnen1lem1  12700  rpnnen1lem3  12701  rpnnen1lem5  12703  rpmulcl  12735  xmulasslem3  13002  xadddilem  13010  ge0mulcl  13175  iccdil  13204  mulmod0  13578  modmulnn  13590  modcyc  13607  modmul1  13625  modaddmulmod  13639  moddi  13640  addmodlteq  13647  reexpcl  13780  reexpclz  13783  expge0  13800  expge1  13801  expubnd  13876  bernneq  13925  expmulnbnd  13931  digit2  13932  digit1  13933  discr  13936  faclbnd  13985  faclbnd3  13987  faclbnd5  13993  facavg  13996  cshweqrep  14515  crre  14806  remim  14809  mulre  14813  sqrlem6  14940  sqrlem7  14941  sqreulem  15052  amgm2  15062  o1mul  15305  caucvgrlem  15365  climcndslem2  15543  climcnds  15544  fprodrecl  15644  fprodreclf  15650  iprodrecl  15693  rerisefaccl  15708  refallfaccl  15709  efcllem  15768  ege2le3  15780  ef01bndlem  15874  cos01gt0  15881  modprm0  16487  prmreclem3  16600  4sqlem11  16637  resubdrg  20794  nmoco  23882  nghmco  23883  blcvx  23942  iihalf1  24075  iihalf2  24077  iimulcl  24081  pcoass  24168  tcphcphlem1  24380  csbren  24544  trirn  24545  minveclem2  24571  sca2rab  24657  uniioombllem5  24732  mbfmulc2lem  24792  i1fmul  24841  i1fmulclem  24848  i1fmulc  24849  dveflem  25124  cmvth  25136  dvivthlem1  25153  dvfsumle  25166  dvfsumlem2  25172  pilem2  25592  tangtx  25643  sinq12gt0  25645  coskpi  25660  cosne0  25666  efif1olem2  25680  efif1olem4  25682  relogexp  25732  logcxp  25805  rpcxpcl  25812  abscxpbnd  25887  ang180lem1  25940  atantan  26054  atanbndlem  26056  o1cxp  26105  divsqrtsumlem  26110  jensenlem2  26118  jensen  26119  zetacvg  26145  regamcl  26191  basellem1  26211  basellem4  26214  basellem9  26219  chtublem  26340  chtub  26341  logfaclbnd  26351  bpos1lem  26411  bposlem1  26413  bposlem2  26414  bposlem6  26418  bposlem7  26419  bposlem9  26421  lgseisen  26508  chebbnd1lem2  26599  chebbnd1lem3  26600  chto1ub  26605  rplogsumlem1  26613  dchrisumlem3  26620  dchrvmasumlem2  26627  dchrisum0lem1b  26644  dchrisum0lem1  26645  dchrisum0lem2  26647  mulog2sumlem1  26663  mulog2sumlem2  26664  log2sumbnd  26673  selberglem2  26675  chpdifbndlem1  26682  logdivbnd  26685  pntrlog2bndlem4  26709  pntibndlem2  26720  pntibndlem3  26721  pntlemh  26728  pntlemr  26731  pntlemk  26735  pntlemo  26736  ostth2lem1  26747  ostth2lem3  26764  ostth3  26767  axcontlem2  27314  nmoub3i  29114  blocni  29146  ubthlem3  29213  minvecolem2  29216  bcs2  29523  nmopub2tALT  30250  nmfnleub2  30267  nmophmi  30372  bdophmi  30373  lnconi  30374  cnlnadjlem2  30409  cnlnadjlem7  30414  nmopadjlem  30430  nmopcoadji  30442  leopnmid  30479  cdj1i  30774  cdj3lem2b  30778  cdj3i  30782  addltmulALT  30787  pnfinf  31416  rezh  31900  sgnmul  32488  sgnmulsgn  32495  sgnmulsgp  32496  signshf  32546  knoppndvlem15  34685  knoppndvlem21  34691  itg2addnclem  35807  ftc1anclem3  35831  isbnd2  35920  isbnd3  35921  equivbnd  35927  2xp3dxp2ge1d  40142  resubdi  40359  pellexlem5  40635  pell1234qrmulcl  40657  pellfundex  40688  rmspecsqrtnq  40708  jm2.24nn  40761  jm2.17a  40762  jm2.17b  40763  jm2.17c  40764  acongrep  40782  acongeq  40785  jm3.1lem2  40820  mulltgt0  42518  ltdiv23neg  42888  fmul01  43075  fmuldfeq  43078  fmul01lt1lem1  43079  fmul01lt1lem2  43080  stoweidlem3  43498  stoweidlem13  43508  stoweidlem17  43512  stoweidlem34  43529  stoweidlem42  43537  stoweidlem48  43543  fourierdlem83  43684  hoidmvlelem2  44088  smfmullem1  44276  2leaddle2  44742  itsclc0lem1  46054  amgmwlem  46458