Theorem remulcl 11237

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  (class class class)co 7430  ℝcr 11151   · cmul 11157

This theorem was proved from axioms:  ax-mulrcl 11215

This theorem is referenced by:  1re  11258  remulcli  11274  remulcld  11288  axmulgt0  11332  00id  11433  mul02lem1  11434  recextlem2  11891  recex  11892  lemul1  12116  ltmul12a  12120  lemul12b  12121  mulgt1OLD  12123  mulgt1  12126  mulge0b  12135  mulle0b  12136  ltdivmul  12140  ledivmul  12141  lt2mul2div  12143  lemuldiv  12145  ltdiv23  12156  lediv23  12157  supmullem2  12236  cju  12259  addltmul  12499  zmulcl  12663  irrmul  13013  rpnnen1lem2  13016  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem5  13020  rpmulcl  13055  xmulasslem3  13324  xadddilem  13332  ge0mulcl  13497  iccdil  13526  mulmod0  13913  modmulnn  13925  modcyc  13942  modmul1  13961  modaddmulmod  13975  moddi  13976  addmodlteq  13983  reexpcl  14115  reexpclz  14119  expge0  14135  expge1  14136  expubnd  14213  bernneq  14264  expmulnbnd  14270  digit2  14271  digit1  14272  discr  14275  faclbnd  14325  faclbnd3  14327  faclbnd5  14333  facavg  14336  cshweqrep  14855  crre  15149  remim  15152  mulre  15156  01sqrexlem6  15282  01sqrexlem7  15283  sqreulem  15394  amgm2  15404  o1mul  15647  caucvgrlem  15705  climcndslem2  15882  climcnds  15883  fprodrecl  15985  fprodreclf  15991  iprodrecl  16034  rerisefaccl  16049  refallfaccl  16050  efcllem  16109  ege2le3  16122  ef01bndlem  16216  cos01gt0  16223  modprm0  16838  prmreclem3  16951  4sqlem11  16988  resubdrg  21643  nmoco  24773  nghmco  24774  blcvx  24833  iihalf1  24971  iihalf2  24974  iimulcl  24979  pcoass  25070  tcphcphlem1  25282  csbren  25446  trirn  25447  minveclem2  25473  sca2rab  25560  uniioombllem5  25635  mbfmulc2lem  25695  i1fmul  25744  i1fmulclem  25751  i1fmulc  25752  dveflem  26031  cmvth  26043  cmvthOLD  26044  dvivthlem1  26061  dvfsumle  26074  dvfsumleOLD  26075  dvfsumlem2  26081  dvfsumlem2OLD  26082  pilem2  26510  tangtx  26561  sinq12gt0  26563  coskpi  26579  cosne0  26585  efif1olem2  26599  efif1olem4  26601  relogexp  26652  logcxp  26725  rpcxpcl  26732  abscxpbnd  26810  ang180lem1  26866  atantan  26980  atanbndlem  26982  o1cxp  27032  divsqrtsumlem  27037  jensenlem2  27045  jensen  27046  zetacvg  27072  regamcl  27118  basellem1  27138  basellem4  27141  basellem9  27146  chtublem  27269  chtub  27270  logfaclbnd  27280  bpos1lem  27340  bposlem1  27342  bposlem2  27343  bposlem6  27347  bposlem7  27348  bposlem9  27350  lgseisen  27437  chebbnd1lem2  27528  chebbnd1lem3  27529  chto1ub  27534  rplogsumlem1  27542  dchrisumlem3  27549  dchrvmasumlem2  27556  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2  27576  mulog2sumlem1  27592  mulog2sumlem2  27593  log2sumbnd  27602  selberglem2  27604  chpdifbndlem1  27611  logdivbnd  27614  pntrlog2bndlem4  27638  pntibndlem2  27649  pntibndlem3  27650  pntlemh  27657  pntlemr  27660  pntlemk  27664  pntlemo  27665  ostth2lem1  27676  ostth2lem3  27693  ostth3  27696  axcontlem2  28994  nmoub3i  30801  blocni  30833  ubthlem3  30900  minvecolem2  30903  bcs2  31210  nmopub2tALT  31937  nmfnleub2  31954  nmophmi  32059  bdophmi  32060  lnconi  32061  cnlnadjlem2  32096  cnlnadjlem7  32101  nmopadjlem  32117  nmopcoadji  32129  leopnmid  32166  cdj1i  32461  cdj3lem2b  32465  cdj3i  32469  addltmulALT  32474  pnfinf  33172  rezh  33931  sgnmul  34523  sgnmulsgn  34530  sgnmulsgp  34531  signshf  34581  knoppndvlem15  36508  knoppndvlem21  36514  itg2addnclem  37657  ftc1anclem3  37681  isbnd2  37769  isbnd3  37770  equivbnd  37776  aks6d1c7lem1  42161  2xp3dxp2ge1d  42222  resubdi  42402  pellexlem5  42820  pell1234qrmulcl  42842  pellfundex  42873  rmspecsqrtnq  42893  jm2.24nn  42947  jm2.17a  42948  jm2.17b  42949  jm2.17c  42950  acongrep  42968  acongeq  42971  jm3.1lem2  43006  mulltgt0  44959  ltdiv23neg  45343  fmul01  45535  fmuldfeq  45538  fmul01lt1lem1  45539  fmul01lt1lem2  45540  stoweidlem3  45958  stoweidlem13  45968  stoweidlem17  45972  stoweidlem34  45989  stoweidlem42  45997  stoweidlem48  46003  fourierdlem83  46144  hoidmvlelem2  46551  smfmullem1  46746  2leaddle2  47247  itsclc0lem1  48605  amgmwlem  49032