Theorem remulcl 11240

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  (class class class)co 7431  ℝcr 11154   · cmul 11160

This theorem was proved from axioms:  ax-mulrcl 11218

This theorem is referenced by:  1re  11261  remulcli  11277  remulcld  11291  axmulgt0  11335  00id  11436  mul02lem1  11437  recextlem2  11894  recex  11895  lemul1  12119  ltmul12a  12123  lemul12b  12124  mulgt1OLD  12126  mulgt1  12129  mulge0b  12138  mulle0b  12139  ltdivmul  12143  ledivmul  12144  lt2mul2div  12146  lemuldiv  12148  ltdiv23  12159  lediv23  12160  supmullem2  12239  cju  12262  addltmul  12502  zmulcl  12666  irrmul  13016  rpnnen1lem2  13019  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  rpmulcl  13058  xmulasslem3  13328  xadddilem  13336  ge0mulcl  13501  iccdil  13530  mulmod0  13917  modmulnn  13929  modcyc  13946  modmul1  13965  modaddmulmod  13979  moddi  13980  addmodlteq  13987  reexpcl  14119  reexpclz  14123  expge0  14139  expge1  14140  expubnd  14217  bernneq  14268  expmulnbnd  14274  digit2  14275  digit1  14276  discr  14279  faclbnd  14329  faclbnd3  14331  faclbnd5  14337  facavg  14340  cshweqrep  14859  crre  15153  remim  15156  mulre  15160  01sqrexlem6  15286  01sqrexlem7  15287  sqreulem  15398  amgm2  15408  o1mul  15651  caucvgrlem  15709  climcndslem2  15886  climcnds  15887  fprodrecl  15989  fprodreclf  15995  iprodrecl  16038  rerisefaccl  16053  refallfaccl  16054  efcllem  16113  ege2le3  16126  ef01bndlem  16220  cos01gt0  16227  modprm0  16843  prmreclem3  16956  4sqlem11  16993  resubdrg  21626  nmoco  24758  nghmco  24759  blcvx  24819  iihalf1  24958  iihalf2  24961  iimulcl  24966  pcoass  25057  tcphcphlem1  25269  csbren  25433  trirn  25434  minveclem2  25460  sca2rab  25547  uniioombllem5  25622  mbfmulc2lem  25682  i1fmul  25731  i1fmulclem  25737  i1fmulc  25738  dveflem  26017  cmvth  26029  cmvthOLD  26030  dvivthlem1  26047  dvfsumle  26060  dvfsumleOLD  26061  dvfsumlem2  26067  dvfsumlem2OLD  26068  pilem2  26496  tangtx  26547  sinq12gt0  26549  coskpi  26565  cosne0  26571  efif1olem2  26585  efif1olem4  26587  relogexp  26638  logcxp  26711  rpcxpcl  26718  abscxpbnd  26796  ang180lem1  26852  atantan  26966  atanbndlem  26968  o1cxp  27018  divsqrtsumlem  27023  jensenlem2  27031  jensen  27032  zetacvg  27058  regamcl  27104  basellem1  27124  basellem4  27127  basellem9  27132  chtublem  27255  chtub  27256  logfaclbnd  27266  bpos1lem  27326  bposlem1  27328  bposlem2  27329  bposlem6  27333  bposlem7  27334  bposlem9  27336  lgseisen  27423  chebbnd1lem2  27514  chebbnd1lem3  27515  chto1ub  27520  rplogsumlem1  27528  dchrisumlem3  27535  dchrvmasumlem2  27542  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2  27562  mulog2sumlem1  27578  mulog2sumlem2  27579  log2sumbnd  27588  selberglem2  27590  chpdifbndlem1  27597  logdivbnd  27600  pntrlog2bndlem4  27624  pntibndlem2  27635  pntibndlem3  27636  pntlemh  27643  pntlemr  27646  pntlemk  27650  pntlemo  27651  ostth2lem1  27662  ostth2lem3  27679  ostth3  27682  axcontlem2  28980  nmoub3i  30792  blocni  30824  ubthlem3  30891  minvecolem2  30894  bcs2  31201  nmopub2tALT  31928  nmfnleub2  31945  nmophmi  32050  bdophmi  32051  lnconi  32052  cnlnadjlem2  32087  cnlnadjlem7  32092  nmopadjlem  32108  nmopcoadji  32120  leopnmid  32157  cdj1i  32452  cdj3lem2b  32456  cdj3i  32460  addltmulALT  32465  pnfinf  33190  rezh  33970  sgnmul  34545  sgnmulsgn  34552  sgnmulsgp  34553  signshf  34603  knoppndvlem15  36527  knoppndvlem21  36533  itg2addnclem  37678  ftc1anclem3  37702  isbnd2  37790  isbnd3  37791  equivbnd  37797  aks6d1c7lem1  42181  2xp3dxp2ge1d  42242  resubdi  42426  pellexlem5  42844  pell1234qrmulcl  42866  pellfundex  42897  rmspecsqrtnq  42917  jm2.24nn  42971  jm2.17a  42972  jm2.17b  42973  jm2.17c  42974  acongrep  42992  acongeq  42995  jm3.1lem2  43030  mulltgt0  45027  ltdiv23neg  45405  fmul01  45595  fmuldfeq  45598  fmul01lt1lem1  45599  fmul01lt1lem2  45600  stoweidlem3  46018  stoweidlem13  46028  stoweidlem17  46032  stoweidlem34  46049  stoweidlem42  46057  stoweidlem48  46063  fourierdlem83  46204  hoidmvlelem2  46611  smfmullem1  46806  2leaddle2  47310  itsclc0lem1  48677  amgmwlem  49321