Theorem remulcl 11086

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  (class class class)co 7341  ℝcr 11000   · cmul 11006

This theorem was proved from axioms:  ax-mulrcl 11064

This theorem is referenced by:  1re  11107  remulcli  11123  remulcld  11137  axmulgt0  11182  00id  11283  mul02lem1  11284  recextlem2  11743  recex  11744  lemul1  11968  ltmul12a  11972  lemul12b  11973  mulgt1OLD  11975  mulgt1  11978  mulge0b  11987  mulle0b  11988  ltdivmul  11992  ledivmul  11993  lt2mul2div  11995  lemuldiv  11997  ltdiv23  12008  lediv23  12009  supmullem2  12088  cju  12116  addltmul  12352  zmulcl  12516  irrmul  12867  rpnnen1lem2  12870  rpnnen1lem1  12871  rpnnen1lem3  12872  rpnnen1lem5  12874  rpmulcl  12910  xmulasslem3  13180  xadddilem  13188  ge0mulcl  13356  iccdil  13385  mulmod0  13776  modmulnn  13788  modcyc  13805  modmul1  13826  modaddmulmod  13840  moddi  13841  addmodlteq  13848  reexpcl  13980  reexpclz  13984  expge0  14000  expge1  14001  expubnd  14080  bernneq  14131  expmulnbnd  14137  digit2  14138  digit1  14139  discr  14142  faclbnd  14192  faclbnd3  14194  faclbnd5  14200  facavg  14203  cshweqrep  14723  crre  15016  remim  15019  mulre  15023  01sqrexlem6  15149  01sqrexlem7  15150  sqreulem  15262  amgm2  15272  o1mul  15517  caucvgrlem  15575  climcndslem2  15752  climcnds  15753  fprodrecl  15855  fprodreclf  15861  iprodrecl  15904  rerisefaccl  15919  refallfaccl  15920  efcllem  15979  ege2le3  15992  ef01bndlem  16088  cos01gt0  16095  modprm0  16712  prmreclem3  16825  4sqlem11  16862  resubdrg  21540  nmoco  24647  nghmco  24648  blcvx  24708  iihalf1  24847  iihalf2  24850  iimulcl  24855  pcoass  24946  tcphcphlem1  25157  csbren  25321  trirn  25322  minveclem2  25348  sca2rab  25435  uniioombllem5  25510  mbfmulc2lem  25570  i1fmul  25619  i1fmulclem  25625  i1fmulc  25626  dveflem  25905  cmvth  25917  cmvthOLD  25918  dvivthlem1  25935  dvfsumle  25948  dvfsumleOLD  25949  dvfsumlem2  25955  dvfsumlem2OLD  25956  pilem2  26384  tangtx  26436  sinq12gt0  26438  coskpi  26454  cosne0  26460  efif1olem2  26474  efif1olem4  26476  relogexp  26527  logcxp  26600  rpcxpcl  26607  abscxpbnd  26685  ang180lem1  26741  atantan  26855  atanbndlem  26857  o1cxp  26907  divsqrtsumlem  26912  jensenlem2  26920  jensen  26921  zetacvg  26947  regamcl  26993  basellem1  27013  basellem4  27016  basellem9  27021  chtublem  27144  chtub  27145  logfaclbnd  27155  bpos1lem  27215  bposlem1  27217  bposlem2  27218  bposlem6  27222  bposlem7  27223  bposlem9  27225  lgseisen  27312  chebbnd1lem2  27403  chebbnd1lem3  27404  chto1ub  27409  rplogsumlem1  27417  dchrisumlem3  27424  dchrvmasumlem2  27431  dchrisum0lem1b  27448  dchrisum0lem1  27449  dchrisum0lem2  27451  mulog2sumlem1  27467  mulog2sumlem2  27468  log2sumbnd  27477  selberglem2  27479  chpdifbndlem1  27486  logdivbnd  27489  pntrlog2bndlem4  27513  pntibndlem2  27524  pntibndlem3  27525  pntlemh  27532  pntlemr  27535  pntlemk  27539  pntlemo  27540  ostth2lem1  27551  ostth2lem3  27568  ostth3  27571  axcontlem2  28938  nmoub3i  30745  blocni  30777  ubthlem3  30844  minvecolem2  30847  bcs2  31154  nmopub2tALT  31881  nmfnleub2  31898  nmophmi  32003  bdophmi  32004  lnconi  32005  cnlnadjlem2  32040  cnlnadjlem7  32045  nmopadjlem  32061  nmopcoadji  32073  leopnmid  32110  cdj1i  32405  cdj3lem2b  32409  cdj3i  32413  addltmulALT  32418  sgnmul  32810  sgnmulsgn  32817  sgnmulsgp  32818  pnfinf  33144  rezh  33974  signshf  34593  knoppndvlem15  36560  knoppndvlem21  36566  itg2addnclem  37711  ftc1anclem3  37735  isbnd2  37823  isbnd3  37824  equivbnd  37830  aks6d1c7lem1  42213  resubdi  42429  pellexlem5  42866  pell1234qrmulcl  42888  pellfundex  42919  rmspecsqrtnq  42939  jm2.24nn  42992  jm2.17a  42993  jm2.17b  42994  jm2.17c  42995  acongrep  43013  acongeq  43016  jm3.1lem2  43051  mulltgt0  45059  ltdiv23neg  45432  fmul01  45620  fmuldfeq  45623  fmul01lt1lem1  45624  fmul01lt1lem2  45625  stoweidlem3  46041  stoweidlem13  46051  stoweidlem17  46055  stoweidlem34  46072  stoweidlem42  46080  stoweidlem48  46086  fourierdlem83  46227  hoidmvlelem2  46634  smfmullem1  46829  2leaddle2  47329  itsclc0lem1  48788  amgmwlem  49834