Theorem remulcl 10779

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  (class class class)co 7191  ℝcr 10693   · cmul 10699

This theorem was proved from axioms:  ax-mulrcl 10757

This theorem is referenced by:  1re  10798  remulcli  10814  remulcld  10828  axmulgt0  10872  00id  10972  mul02lem1  10973  recextlem2  11428  recex  11429  lemul1  11649  ltmul12a  11653  lemul12b  11654  mulgt1  11656  mulge0b  11667  mulle0b  11668  ltdivmul  11672  ledivmul  11673  lt2mul2div  11675  lemuldiv  11677  ltdiv23  11688  lediv23  11689  supmullem2  11768  cju  11791  addltmul  12031  zmulcl  12191  irrmul  12535  rpnnen1lem2  12538  rpnnen1lem1  12539  rpnnen1lem3  12540  rpnnen1lem5  12542  rpmulcl  12574  xmulasslem3  12841  xadddilem  12849  ge0mulcl  13014  iccdil  13043  mulmod0  13415  modmulnn  13427  modcyc  13444  modmul1  13462  modaddmulmod  13476  moddi  13477  addmodlteq  13484  reexpcl  13617  reexpclz  13620  expge0  13636  expge1  13637  expubnd  13712  bernneq  13761  expmulnbnd  13767  digit2  13768  digit1  13769  discr  13772  faclbnd  13821  faclbnd3  13823  faclbnd5  13829  facavg  13832  cshweqrep  14351  crre  14642  remim  14645  mulre  14649  sqrlem6  14776  sqrlem7  14777  sqreulem  14888  amgm2  14898  o1mul  15141  caucvgrlem  15201  climcndslem2  15377  climcnds  15378  fprodrecl  15478  fprodreclf  15484  iprodrecl  15527  rerisefaccl  15542  refallfaccl  15543  efcllem  15602  ege2le3  15614  ef01bndlem  15708  cos01gt0  15715  modprm0  16321  prmreclem3  16434  4sqlem11  16471  resubdrg  20524  nmoco  23589  nghmco  23590  blcvx  23649  iihalf1  23782  iihalf2  23784  iimulcl  23788  pcoass  23875  tcphcphlem1  24086  csbren  24250  trirn  24251  minveclem2  24277  sca2rab  24363  uniioombllem5  24438  mbfmulc2lem  24498  i1fmul  24547  i1fmulclem  24554  i1fmulc  24555  dveflem  24830  cmvth  24842  dvivthlem1  24859  dvfsumle  24872  dvfsumlem2  24878  pilem2  25298  tangtx  25349  sinq12gt0  25351  coskpi  25366  cosne0  25372  efif1olem2  25386  efif1olem4  25388  relogexp  25438  logcxp  25511  rpcxpcl  25518  abscxpbnd  25593  ang180lem1  25646  atantan  25760  atanbndlem  25762  o1cxp  25811  divsqrtsumlem  25816  jensenlem2  25824  jensen  25825  zetacvg  25851  regamcl  25897  basellem1  25917  basellem4  25920  basellem9  25925  chtublem  26046  chtub  26047  logfaclbnd  26057  bpos1lem  26117  bposlem1  26119  bposlem2  26120  bposlem6  26124  bposlem7  26125  bposlem9  26127  lgseisen  26214  chebbnd1lem2  26305  chebbnd1lem3  26306  chto1ub  26311  rplogsumlem1  26319  dchrisumlem3  26326  dchrvmasumlem2  26333  dchrisum0lem1b  26350  dchrisum0lem1  26351  dchrisum0lem2  26353  mulog2sumlem1  26369  mulog2sumlem2  26370  log2sumbnd  26379  selberglem2  26381  chpdifbndlem1  26388  logdivbnd  26391  pntrlog2bndlem4  26415  pntibndlem2  26426  pntibndlem3  26427  pntlemh  26434  pntlemr  26437  pntlemk  26441  pntlemo  26442  ostth2lem1  26453  ostth2lem3  26470  ostth3  26473  axcontlem2  27010  nmoub3i  28808  blocni  28840  ubthlem3  28907  minvecolem2  28910  bcs2  29217  nmopub2tALT  29944  nmfnleub2  29961  nmophmi  30066  bdophmi  30067  lnconi  30068  cnlnadjlem2  30103  cnlnadjlem7  30108  nmopadjlem  30124  nmopcoadji  30136  leopnmid  30173  cdj1i  30468  cdj3lem2b  30472  cdj3i  30476  addltmulALT  30481  pnfinf  31110  rezh  31587  sgnmul  32175  sgnmulsgn  32182  sgnmulsgp  32183  signshf  32233  knoppndvlem15  34392  knoppndvlem21  34398  itg2addnclem  35514  ftc1anclem3  35538  isbnd2  35627  isbnd3  35628  equivbnd  35634  2xp3dxp2ge1d  39825  resubdi  40028  pellexlem5  40299  pell1234qrmulcl  40321  pellfundex  40352  rmspecsqrtnq  40372  jm2.24nn  40425  jm2.17a  40426  jm2.17b  40427  jm2.17c  40428  acongrep  40446  acongeq  40449  jm3.1lem2  40484  mulltgt0  42179  ltdiv23neg  42548  fmul01  42739  fmuldfeq  42742  fmul01lt1lem1  42743  fmul01lt1lem2  42744  stoweidlem3  43162  stoweidlem13  43172  stoweidlem17  43176  stoweidlem34  43193  stoweidlem42  43201  stoweidlem48  43207  fourierdlem83  43348  hoidmvlelem2  43752  smfmullem1  43940  2leaddle2  44406  itsclc0lem1  45718  amgmwlem  46120