Theorem remulcl 11123

Description: Alias for ax-mulrcl 11101, for naming consistency with remulcli 11160. (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 7368  ℝcr 11037   · cmul 11043

This theorem was proved from axioms:  ax-mulrcl 11101

This theorem is referenced by:  1re  11144  remulcli  11160  remulcld  11174  axmulgt0  11219  00id  11320  mul02lem1  11321  recextlem2  11780  recex  11781  lemul1  12005  ltmul12a  12009  lemul12b  12010  mulgt1OLD  12012  mulgt1  12015  mulge0b  12024  mulle0b  12025  ltdivmul  12029  ledivmul  12030  lt2mul2div  12032  lemuldiv  12034  ltdiv23  12045  lediv23  12046  supmullem2  12125  cju  12153  addltmul  12389  zmulcl  12552  irrmul  12899  rpnnen1lem2  12902  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  rpmulcl  12942  xmulasslem3  13213  xadddilem  13221  ge0mulcl  13389  iccdil  13418  mulmod0  13809  modmulnn  13821  modcyc  13838  modmul1  13859  modaddmulmod  13873  moddi  13874  addmodlteq  13881  reexpcl  14013  reexpclz  14017  expge0  14033  expge1  14034  expubnd  14113  bernneq  14164  expmulnbnd  14170  digit2  14171  digit1  14172  discr  14175  faclbnd  14225  faclbnd3  14227  faclbnd5  14233  facavg  14236  cshweqrep  14756  crre  15049  remim  15052  mulre  15056  01sqrexlem6  15182  01sqrexlem7  15183  sqreulem  15295  amgm2  15305  o1mul  15550  caucvgrlem  15608  climcndslem2  15785  climcnds  15786  fprodrecl  15888  fprodreclf  15894  iprodrecl  15937  rerisefaccl  15952  refallfaccl  15953  efcllem  16012  ege2le3  16025  ef01bndlem  16121  cos01gt0  16128  modprm0  16745  prmreclem3  16858  4sqlem11  16895  resubdrg  21575  nmoco  24693  nghmco  24694  blcvx  24754  iihalf1  24893  iihalf2  24896  iimulcl  24901  pcoass  24992  tcphcphlem1  25203  csbren  25367  trirn  25368  minveclem2  25394  sca2rab  25481  uniioombllem5  25556  mbfmulc2lem  25616  i1fmul  25665  i1fmulclem  25671  i1fmulc  25672  dveflem  25951  cmvth  25963  cmvthOLD  25964  dvivthlem1  25981  dvfsumle  25994  dvfsumleOLD  25995  dvfsumlem2  26001  dvfsumlem2OLD  26002  pilem2  26430  tangtx  26482  sinq12gt0  26484  coskpi  26500  cosne0  26506  efif1olem2  26520  efif1olem4  26522  relogexp  26573  logcxp  26646  rpcxpcl  26653  abscxpbnd  26731  ang180lem1  26787  atantan  26901  atanbndlem  26903  o1cxp  26953  divsqrtsumlem  26958  jensenlem2  26966  jensen  26967  zetacvg  26993  regamcl  27039  basellem1  27059  basellem4  27062  basellem9  27067  chtublem  27190  chtub  27191  logfaclbnd  27201  bpos1lem  27261  bposlem1  27263  bposlem2  27264  bposlem6  27268  bposlem7  27269  bposlem9  27271  lgseisen  27358  chebbnd1lem2  27449  chebbnd1lem3  27450  chto1ub  27455  rplogsumlem1  27463  dchrisumlem3  27470  dchrvmasumlem2  27477  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2  27497  mulog2sumlem1  27513  mulog2sumlem2  27514  log2sumbnd  27523  selberglem2  27525  chpdifbndlem1  27532  logdivbnd  27535  pntrlog2bndlem4  27559  pntibndlem2  27570  pntibndlem3  27571  pntlemh  27578  pntlemr  27581  pntlemk  27585  pntlemo  27586  ostth2lem1  27597  ostth2lem3  27614  ostth3  27617  axcontlem2  29050  nmoub3i  30861  blocni  30893  ubthlem3  30960  minvecolem2  30963  bcs2  31270  nmopub2tALT  31997  nmfnleub2  32014  nmophmi  32119  bdophmi  32120  lnconi  32121  cnlnadjlem2  32156  cnlnadjlem7  32161  nmopadjlem  32177  nmopcoadji  32189  leopnmid  32226  cdj1i  32521  cdj3lem2b  32525  cdj3i  32529  addltmulALT  32534  sgnmul  32927  sgnmulsgn  32934  sgnmulsgp  32935  pnfinf  33277  rezh  34147  signshf  34766  knoppndvlem15  36748  knoppndvlem21  36754  itg2addnclem  37922  ftc1anclem3  37946  isbnd2  38034  isbnd3  38035  equivbnd  38041  aks6d1c7lem1  42550  resubdi  42766  pellexlem5  43190  pell1234qrmulcl  43212  pellfundex  43243  rmspecsqrtnq  43263  jm2.24nn  43316  jm2.17a  43317  jm2.17b  43318  jm2.17c  43319  acongrep  43337  acongeq  43340  jm3.1lem2  43375  mulltgt0  45382  ltdiv23neg  45752  fmul01  45940  fmuldfeq  45943  fmul01lt1lem1  45944  fmul01lt1lem2  45945  stoweidlem3  46361  stoweidlem13  46371  stoweidlem17  46375  stoweidlem34  46392  stoweidlem42  46400  stoweidlem48  46406  fourierdlem83  46547  hoidmvlelem2  46954  smfmullem1  47149  2leaddle2  47658  itsclc0lem1  49116  amgmwlem  50161