Theorem remulcl 11123

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037   · cmul 11043

This theorem was proved from axioms:  ax-mulrcl 11101

This theorem is referenced by:  1re  11144  remulcli  11161  remulcld  11175  axmulgt0  11220  00id  11321  mul02lem1  11322  recextlem2  11781  recex  11782  lemul1  12007  ltmul12a  12011  lemul12b  12012  mulgt1OLD  12014  mulgt1  12017  mulge0b  12026  mulle0b  12027  ltdivmul  12031  ledivmul  12032  lt2mul2div  12034  lemuldiv  12036  ltdiv23  12047  lediv23  12048  supmullem2  12127  cju  12155  addltmul  12413  zmulcl  12576  irrmul  12924  rpnnen1lem2  12927  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  rpmulcl  12967  xmulasslem3  13238  xadddilem  13246  ge0mulcl  13414  iccdil  13443  mulmod0  13836  modmulnn  13848  modcyc  13865  modmul1  13886  modaddmulmod  13900  moddi  13901  addmodlteq  13908  reexpcl  14040  reexpclz  14044  expge0  14060  expge1  14061  expubnd  14140  bernneq  14191  expmulnbnd  14197  digit2  14198  digit1  14199  discr  14202  faclbnd  14252  faclbnd3  14254  faclbnd5  14260  facavg  14263  cshweqrep  14783  crre  15076  remim  15079  mulre  15083  01sqrexlem6  15209  01sqrexlem7  15210  sqreulem  15322  amgm2  15332  o1mul  15577  caucvgrlem  15635  climcndslem2  15815  climcnds  15816  fprodrecl  15918  fprodreclf  15924  iprodrecl  15967  rerisefaccl  15982  refallfaccl  15983  efcllem  16042  ege2le3  16055  ef01bndlem  16151  cos01gt0  16158  modprm0  16776  prmreclem3  16889  4sqlem11  16926  resubdrg  21588  nmoco  24702  nghmco  24703  blcvx  24763  iihalf1  24898  iihalf2  24900  iimulcl  24904  pcoass  24991  tcphcphlem1  25202  csbren  25366  trirn  25367  minveclem2  25393  sca2rab  25479  uniioombllem5  25554  mbfmulc2lem  25614  i1fmul  25663  i1fmulclem  25669  i1fmulc  25670  dveflem  25946  cmvth  25958  dvivthlem1  25975  dvfsumle  25988  dvfsumlem2  25994  pilem2  26417  tangtx  26469  sinq12gt0  26471  coskpi  26487  cosne0  26493  efif1olem2  26507  efif1olem4  26509  relogexp  26560  logcxp  26633  rpcxpcl  26640  abscxpbnd  26717  ang180lem1  26773  atantan  26887  atanbndlem  26889  o1cxp  26938  divsqrtsumlem  26943  jensenlem2  26951  jensen  26952  zetacvg  26978  regamcl  27024  basellem1  27044  basellem4  27047  basellem9  27052  chtublem  27174  chtub  27175  logfaclbnd  27185  bpos1lem  27245  bposlem1  27247  bposlem2  27248  bposlem6  27252  bposlem7  27253  bposlem9  27255  lgseisen  27342  chebbnd1lem2  27433  chebbnd1lem3  27434  chto1ub  27439  rplogsumlem1  27447  dchrisumlem3  27454  dchrvmasumlem2  27461  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2  27481  mulog2sumlem1  27497  mulog2sumlem2  27498  log2sumbnd  27507  selberglem2  27509  chpdifbndlem1  27516  logdivbnd  27519  pntrlog2bndlem4  27543  pntibndlem2  27554  pntibndlem3  27555  pntlemh  27562  pntlemr  27565  pntlemk  27569  pntlemo  27570  ostth2lem1  27581  ostth2lem3  27598  ostth3  27601  axcontlem2  29034  nmoub3i  30844  blocni  30876  ubthlem3  30943  minvecolem2  30946  bcs2  31253  nmopub2tALT  31980  nmfnleub2  31997  nmophmi  32102  bdophmi  32103  lnconi  32104  cnlnadjlem2  32139  cnlnadjlem7  32144  nmopadjlem  32160  nmopcoadji  32172  leopnmid  32209  cdj1i  32504  cdj3lem2b  32508  cdj3i  32512  addltmulALT  32517  sgnmul  32908  sgnmulsgn  32915  sgnmulsgp  32916  pnfinf  33244  rezh  34113  signshf  34732  knoppndvlem15  36786  knoppndvlem21  36792  itg2addnclem  37992  ftc1anclem3  38016  isbnd2  38104  isbnd3  38105  equivbnd  38111  aks6d1c7lem1  42619  resubdi  42828  pellexlem5  43261  pell1234qrmulcl  43283  pellfundex  43314  rmspecsqrtnq  43334  jm2.24nn  43387  jm2.17a  43388  jm2.17b  43389  jm2.17c  43390  acongrep  43408  acongeq  43411  jm3.1lem2  43446  mulltgt0  45453  ltdiv23neg  45823  fmul01  46010  fmuldfeq  46013  fmul01lt1lem1  46014  fmul01lt1lem2  46015  stoweidlem3  46431  stoweidlem13  46441  stoweidlem17  46445  stoweidlem34  46462  stoweidlem42  46470  stoweidlem48  46476  fourierdlem83  46617  hoidmvlelem2  47024  smfmullem1  47219  2leaddle2  47746  itsclc0lem1  49232  amgmwlem  50277