Theorem remulcl 10622

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  (class class class)co 7156  ℝcr 10536   · cmul 10542

This theorem was proved from axioms:  ax-mulrcl 10600

This theorem is referenced by:  1re  10641  remulcli  10657  remulcld  10671  axmulgt0  10715  00id  10815  mul02lem1  10816  recextlem2  11271  recex  11272  lemul1  11492  ltmul12a  11496  lemul12b  11497  mulgt1  11499  mulge0b  11510  mulle0b  11511  ltdivmul  11515  ledivmul  11516  lt2mul2div  11518  lemuldiv  11520  ltdiv23  11531  lediv23  11532  supmullem2  11612  cju  11634  addltmul  11874  zmulcl  12032  irrmul  12374  rpnnen1lem2  12377  rpnnen1lem1  12378  rpnnen1lem3  12379  rpnnen1lem5  12381  rpmulcl  12413  xmulasslem3  12680  xadddilem  12688  ge0mulcl  12850  iccdil  12877  mulmod0  13246  modmulnn  13258  modcyc  13275  modmul1  13293  modaddmulmod  13307  moddi  13308  addmodlteq  13315  reexpcl  13447  reexpclz  13450  expge0  13466  expge1  13467  expubnd  13542  bernneq  13591  expmulnbnd  13597  digit2  13598  digit1  13599  discr  13602  faclbnd  13651  faclbnd3  13653  faclbnd5  13659  facavg  13662  cshweqrep  14183  crre  14473  remim  14476  mulre  14480  sqrlem6  14607  sqrlem7  14608  sqreulem  14719  amgm2  14729  o1mul  14971  caucvgrlem  15029  climcndslem2  15205  climcnds  15206  fprodrecl  15307  fprodreclf  15313  iprodrecl  15356  rerisefaccl  15371  refallfaccl  15372  efcllem  15431  ege2le3  15443  ef01bndlem  15537  cos01gt0  15544  modprm0  16142  prmreclem3  16254  4sqlem11  16291  resubdrg  20752  nmoco  23346  nghmco  23347  blcvx  23406  iihalf1  23535  iihalf2  23537  iimulcl  23541  pcoass  23628  tcphcphlem1  23838  csbren  24002  trirn  24003  minveclem2  24029  sca2rab  24113  uniioombllem5  24188  mbfmulc2lem  24248  i1fmul  24297  i1fmulclem  24303  i1fmulc  24304  dveflem  24576  cmvth  24588  dvivthlem1  24605  dvfsumle  24618  dvfsumlem2  24624  pilem2  25040  tangtx  25091  sinq12gt0  25093  coskpi  25108  cosne0  25114  efif1olem2  25127  efif1olem4  25129  relogexp  25179  logcxp  25252  rpcxpcl  25259  abscxpbnd  25334  ang180lem1  25387  atantan  25501  atanbndlem  25503  o1cxp  25552  divsqrtsumlem  25557  jensenlem2  25565  jensen  25566  zetacvg  25592  regamcl  25638  basellem1  25658  basellem4  25661  basellem9  25666  chtublem  25787  chtub  25788  logfaclbnd  25798  bpos1lem  25858  bposlem1  25860  bposlem2  25861  bposlem6  25865  bposlem7  25866  bposlem9  25868  lgseisen  25955  chebbnd1lem2  26046  chebbnd1lem3  26047  chto1ub  26052  rplogsumlem1  26060  dchrisumlem3  26067  dchrvmasumlem2  26074  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2  26094  mulog2sumlem1  26110  mulog2sumlem2  26111  log2sumbnd  26120  selberglem2  26122  chpdifbndlem1  26129  logdivbnd  26132  pntrlog2bndlem4  26156  pntibndlem2  26167  pntibndlem3  26168  pntlemh  26175  pntlemr  26178  pntlemk  26182  pntlemo  26183  ostth2lem1  26194  ostth2lem3  26211  ostth3  26214  axcontlem2  26751  nmoub3i  28550  blocni  28582  ubthlem3  28649  minvecolem2  28652  bcs2  28959  nmopub2tALT  29686  nmfnleub2  29703  nmophmi  29808  bdophmi  29809  lnconi  29810  cnlnadjlem2  29845  cnlnadjlem7  29850  nmopadjlem  29866  nmopcoadji  29878  leopnmid  29915  cdj1i  30210  cdj3lem2b  30214  cdj3i  30218  addltmulALT  30223  pnfinf  30812  rezh  31212  sgnmul  31800  sgnmulsgn  31807  sgnmulsgp  31808  signshf  31858  knoppndvlem15  33865  knoppndvlem21  33871  itg2addnclem  34958  ftc1anclem3  34984  isbnd2  35076  isbnd3  35077  equivbnd  35083  2xp3dxp2ge1d  39117  resubdi  39246  pellexlem5  39450  pell1234qrmulcl  39472  pellfundex  39503  rmspecsqrtnq  39523  jm2.24nn  39576  jm2.17a  39577  jm2.17b  39578  jm2.17c  39579  acongrep  39597  acongeq  39600  jm3.1lem2  39635  mulltgt0  41299  ltdiv23neg  41686  fmul01  41881  fmuldfeq  41884  fmul01lt1lem1  41885  fmul01lt1lem2  41886  stoweidlem3  42308  stoweidlem13  42318  stoweidlem17  42322  stoweidlem34  42339  stoweidlem42  42347  stoweidlem48  42353  fourierdlem83  42494  hoidmvlelem2  42898  smfmullem1  43086  2leaddle2  43518  itsclc0lem1  44763  amgmwlem  44923