Theorem remulcl 11057

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2105  (class class class)co 7337  ℝcr 10971   · cmul 10977

This theorem was proved from axioms:  ax-mulrcl 11035

This theorem is referenced by:  1re  11076  remulcli  11092  remulcld  11106  axmulgt0  11150  00id  11251  mul02lem1  11252  recextlem2  11707  recex  11708  lemul1  11928  ltmul12a  11932  lemul12b  11933  mulgt1  11935  mulge0b  11946  mulle0b  11947  ltdivmul  11951  ledivmul  11952  lt2mul2div  11954  lemuldiv  11956  ltdiv23  11967  lediv23  11968  supmullem2  12047  cju  12070  addltmul  12310  zmulcl  12470  irrmul  12815  rpnnen1lem2  12818  rpnnen1lem1  12819  rpnnen1lem3  12820  rpnnen1lem5  12822  rpmulcl  12854  xmulasslem3  13121  xadddilem  13129  ge0mulcl  13294  iccdil  13323  mulmod0  13698  modmulnn  13710  modcyc  13727  modmul1  13745  modaddmulmod  13759  moddi  13760  addmodlteq  13767  reexpcl  13900  reexpclz  13903  expge0  13920  expge1  13921  expubnd  13996  bernneq  14045  expmulnbnd  14051  digit2  14052  digit1  14053  discr  14056  faclbnd  14105  faclbnd3  14107  faclbnd5  14113  facavg  14116  cshweqrep  14632  crre  14924  remim  14927  mulre  14931  sqrlem6  15058  sqrlem7  15059  sqreulem  15170  amgm2  15180  o1mul  15423  caucvgrlem  15483  climcndslem2  15661  climcnds  15662  fprodrecl  15762  fprodreclf  15768  iprodrecl  15811  rerisefaccl  15826  refallfaccl  15827  efcllem  15886  ege2le3  15898  ef01bndlem  15992  cos01gt0  15999  modprm0  16603  prmreclem3  16716  4sqlem11  16753  resubdrg  20919  nmoco  24007  nghmco  24008  blcvx  24067  iihalf1  24200  iihalf2  24202  iimulcl  24206  pcoass  24293  tcphcphlem1  24505  csbren  24669  trirn  24670  minveclem2  24696  sca2rab  24782  uniioombllem5  24857  mbfmulc2lem  24917  i1fmul  24966  i1fmulclem  24973  i1fmulc  24974  dveflem  25249  cmvth  25261  dvivthlem1  25278  dvfsumle  25291  dvfsumlem2  25297  pilem2  25717  tangtx  25768  sinq12gt0  25770  coskpi  25785  cosne0  25791  efif1olem2  25805  efif1olem4  25807  relogexp  25857  logcxp  25930  rpcxpcl  25937  abscxpbnd  26012  ang180lem1  26065  atantan  26179  atanbndlem  26181  o1cxp  26230  divsqrtsumlem  26235  jensenlem2  26243  jensen  26244  zetacvg  26270  regamcl  26316  basellem1  26336  basellem4  26339  basellem9  26344  chtublem  26465  chtub  26466  logfaclbnd  26476  bpos1lem  26536  bposlem1  26538  bposlem2  26539  bposlem6  26543  bposlem7  26544  bposlem9  26546  lgseisen  26633  chebbnd1lem2  26724  chebbnd1lem3  26725  chto1ub  26730  rplogsumlem1  26738  dchrisumlem3  26745  dchrvmasumlem2  26752  dchrisum0lem1b  26769  dchrisum0lem1  26770  dchrisum0lem2  26772  mulog2sumlem1  26788  mulog2sumlem2  26789  log2sumbnd  26798  selberglem2  26800  chpdifbndlem1  26807  logdivbnd  26810  pntrlog2bndlem4  26834  pntibndlem2  26845  pntibndlem3  26846  pntlemh  26853  pntlemr  26856  pntlemk  26860  pntlemo  26861  ostth2lem1  26872  ostth2lem3  26889  ostth3  26892  axcontlem2  27622  nmoub3i  29423  blocni  29455  ubthlem3  29522  minvecolem2  29525  bcs2  29832  nmopub2tALT  30559  nmfnleub2  30576  nmophmi  30681  bdophmi  30682  lnconi  30683  cnlnadjlem2  30718  cnlnadjlem7  30723  nmopadjlem  30739  nmopcoadji  30751  leopnmid  30788  cdj1i  31083  cdj3lem2b  31087  cdj3i  31091  addltmulALT  31096  pnfinf  31724  rezh  32219  sgnmul  32809  sgnmulsgn  32816  sgnmulsgp  32817  signshf  32867  knoppndvlem15  34802  knoppndvlem21  34808  itg2addnclem  35941  ftc1anclem3  35965  isbnd2  36054  isbnd3  36055  equivbnd  36061  2xp3dxp2ge1d  40427  resubdi  40647  pellexlem5  40925  pell1234qrmulcl  40947  pellfundex  40978  rmspecsqrtnq  40998  jm2.24nn  41052  jm2.17a  41053  jm2.17b  41054  jm2.17c  41055  acongrep  41073  acongeq  41076  jm3.1lem2  41111  mulltgt0  42894  ltdiv23neg  43277  fmul01  43465  fmuldfeq  43468  fmul01lt1lem1  43469  fmul01lt1lem2  43470  stoweidlem3  43888  stoweidlem13  43898  stoweidlem17  43902  stoweidlem34  43919  stoweidlem42  43927  stoweidlem48  43933  fourierdlem83  44074  hoidmvlelem2  44479  smfmullem1  44674  2leaddle2  45149  itsclc0lem1  46461  amgmwlem  46865