Theorem remulcl 11219

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7410  ℝcr 11133   · cmul 11139

This theorem was proved from axioms:  ax-mulrcl 11197

This theorem is referenced by:  1re  11240  remulcli  11256  remulcld  11270  axmulgt0  11314  00id  11415  mul02lem1  11416  recextlem2  11873  recex  11874  lemul1  12098  ltmul12a  12102  lemul12b  12103  mulgt1OLD  12105  mulgt1  12108  mulge0b  12117  mulle0b  12118  ltdivmul  12122  ledivmul  12123  lt2mul2div  12125  lemuldiv  12127  ltdiv23  12138  lediv23  12139  supmullem2  12218  cju  12241  addltmul  12482  zmulcl  12646  irrmul  12995  rpnnen1lem2  12998  rpnnen1lem1  12999  rpnnen1lem3  13000  rpnnen1lem5  13002  rpmulcl  13037  xmulasslem3  13307  xadddilem  13315  ge0mulcl  13483  iccdil  13512  mulmod0  13899  modmulnn  13911  modcyc  13928  modmul1  13947  modaddmulmod  13961  moddi  13962  addmodlteq  13969  reexpcl  14101  reexpclz  14105  expge0  14121  expge1  14122  expubnd  14201  bernneq  14252  expmulnbnd  14258  digit2  14259  digit1  14260  discr  14263  faclbnd  14313  faclbnd3  14315  faclbnd5  14321  facavg  14324  cshweqrep  14844  crre  15138  remim  15141  mulre  15145  01sqrexlem6  15271  01sqrexlem7  15272  sqreulem  15383  amgm2  15393  o1mul  15636  caucvgrlem  15694  climcndslem2  15871  climcnds  15872  fprodrecl  15974  fprodreclf  15980  iprodrecl  16023  rerisefaccl  16038  refallfaccl  16039  efcllem  16098  ege2le3  16111  ef01bndlem  16207  cos01gt0  16214  modprm0  16830  prmreclem3  16943  4sqlem11  16980  resubdrg  21573  nmoco  24681  nghmco  24682  blcvx  24742  iihalf1  24881  iihalf2  24884  iimulcl  24889  pcoass  24980  tcphcphlem1  25192  csbren  25356  trirn  25357  minveclem2  25383  sca2rab  25470  uniioombllem5  25545  mbfmulc2lem  25605  i1fmul  25654  i1fmulclem  25660  i1fmulc  25661  dveflem  25940  cmvth  25952  cmvthOLD  25953  dvivthlem1  25970  dvfsumle  25983  dvfsumleOLD  25984  dvfsumlem2  25990  dvfsumlem2OLD  25991  pilem2  26419  tangtx  26471  sinq12gt0  26473  coskpi  26489  cosne0  26495  efif1olem2  26509  efif1olem4  26511  relogexp  26562  logcxp  26635  rpcxpcl  26642  abscxpbnd  26720  ang180lem1  26776  atantan  26890  atanbndlem  26892  o1cxp  26942  divsqrtsumlem  26947  jensenlem2  26955  jensen  26956  zetacvg  26982  regamcl  27028  basellem1  27048  basellem4  27051  basellem9  27056  chtublem  27179  chtub  27180  logfaclbnd  27190  bpos1lem  27250  bposlem1  27252  bposlem2  27253  bposlem6  27257  bposlem7  27258  bposlem9  27260  lgseisen  27347  chebbnd1lem2  27438  chebbnd1lem3  27439  chto1ub  27444  rplogsumlem1  27452  dchrisumlem3  27459  dchrvmasumlem2  27466  dchrisum0lem1b  27483  dchrisum0lem1  27484  dchrisum0lem2  27486  mulog2sumlem1  27502  mulog2sumlem2  27503  log2sumbnd  27512  selberglem2  27514  chpdifbndlem1  27521  logdivbnd  27524  pntrlog2bndlem4  27548  pntibndlem2  27559  pntibndlem3  27560  pntlemh  27567  pntlemr  27570  pntlemk  27574  pntlemo  27575  ostth2lem1  27586  ostth2lem3  27603  ostth3  27606  axcontlem2  28949  nmoub3i  30759  blocni  30791  ubthlem3  30858  minvecolem2  30861  bcs2  31168  nmopub2tALT  31895  nmfnleub2  31912  nmophmi  32017  bdophmi  32018  lnconi  32019  cnlnadjlem2  32054  cnlnadjlem7  32059  nmopadjlem  32075  nmopcoadji  32087  leopnmid  32124  cdj1i  32419  cdj3lem2b  32423  cdj3i  32427  addltmulALT  32432  sgnmul  32819  sgnmulsgn  32826  sgnmulsgp  32827  pnfinf  33186  rezh  34005  signshf  34625  knoppndvlem15  36549  knoppndvlem21  36555  itg2addnclem  37700  ftc1anclem3  37724  isbnd2  37812  isbnd3  37813  equivbnd  37819  aks6d1c7lem1  42198  resubdi  42406  pellexlem5  42823  pell1234qrmulcl  42845  pellfundex  42876  rmspecsqrtnq  42896  jm2.24nn  42950  jm2.17a  42951  jm2.17b  42952  jm2.17c  42953  acongrep  42971  acongeq  42974  jm3.1lem2  43009  mulltgt0  45013  ltdiv23neg  45388  fmul01  45576  fmuldfeq  45579  fmul01lt1lem1  45580  fmul01lt1lem2  45581  stoweidlem3  45999  stoweidlem13  46009  stoweidlem17  46013  stoweidlem34  46030  stoweidlem42  46038  stoweidlem48  46044  fourierdlem83  46185  hoidmvlelem2  46592  smfmullem1  46787  2leaddle2  47294  itsclc0lem1  48703  amgmwlem  49633