Theorem remulcl 11225

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098  (class class class)co 7419  ℝcr 11139   · cmul 11145

This theorem was proved from axioms:  ax-mulrcl 11203

This theorem is referenced by:  1re  11246  remulcli  11262  remulcld  11276  axmulgt0  11320  00id  11421  mul02lem1  11422  recextlem2  11877  recex  11878  lemul1  12099  ltmul12a  12103  lemul12b  12104  mulgt1  12106  mulge0b  12117  mulle0b  12118  ltdivmul  12122  ledivmul  12123  lt2mul2div  12125  lemuldiv  12127  ltdiv23  12138  lediv23  12139  supmullem2  12218  cju  12241  addltmul  12481  zmulcl  12644  irrmul  12991  rpnnen1lem2  12994  rpnnen1lem1  12995  rpnnen1lem3  12996  rpnnen1lem5  12998  rpmulcl  13032  xmulasslem3  13300  xadddilem  13308  ge0mulcl  13473  iccdil  13502  mulmod0  13878  modmulnn  13890  modcyc  13907  modmul1  13925  modaddmulmod  13939  moddi  13940  addmodlteq  13947  reexpcl  14079  reexpclz  14083  expge0  14099  expge1  14100  expubnd  14177  bernneq  14227  expmulnbnd  14233  digit2  14234  digit1  14235  discr  14238  faclbnd  14285  faclbnd3  14287  faclbnd5  14293  facavg  14296  cshweqrep  14807  crre  15097  remim  15100  mulre  15104  01sqrexlem6  15230  01sqrexlem7  15231  sqreulem  15342  amgm2  15352  o1mul  15595  caucvgrlem  15655  climcndslem2  15832  climcnds  15833  fprodrecl  15933  fprodreclf  15939  iprodrecl  15982  rerisefaccl  15997  refallfaccl  15998  efcllem  16057  ege2le3  16070  ef01bndlem  16164  cos01gt0  16171  modprm0  16777  prmreclem3  16890  4sqlem11  16927  resubdrg  21557  nmoco  24698  nghmco  24699  blcvx  24758  iihalf1  24896  iihalf2  24899  iimulcl  24904  pcoass  24995  tcphcphlem1  25207  csbren  25371  trirn  25372  minveclem2  25398  sca2rab  25485  uniioombllem5  25560  mbfmulc2lem  25620  i1fmul  25669  i1fmulclem  25676  i1fmulc  25677  dveflem  25955  cmvth  25967  cmvthOLD  25968  dvivthlem1  25985  dvfsumle  25998  dvfsumleOLD  25999  dvfsumlem2  26005  dvfsumlem2OLD  26006  pilem2  26434  tangtx  26485  sinq12gt0  26487  coskpi  26502  cosne0  26508  efif1olem2  26522  efif1olem4  26524  relogexp  26575  logcxp  26648  rpcxpcl  26655  abscxpbnd  26733  ang180lem1  26786  atantan  26900  atanbndlem  26902  o1cxp  26952  divsqrtsumlem  26957  jensenlem2  26965  jensen  26966  zetacvg  26992  regamcl  27038  basellem1  27058  basellem4  27061  basellem9  27066  chtublem  27189  chtub  27190  logfaclbnd  27200  bpos1lem  27260  bposlem1  27262  bposlem2  27263  bposlem6  27267  bposlem7  27268  bposlem9  27270  lgseisen  27357  chebbnd1lem2  27448  chebbnd1lem3  27449  chto1ub  27454  rplogsumlem1  27462  dchrisumlem3  27469  dchrvmasumlem2  27476  dchrisum0lem1b  27493  dchrisum0lem1  27494  dchrisum0lem2  27496  mulog2sumlem1  27512  mulog2sumlem2  27513  log2sumbnd  27522  selberglem2  27524  chpdifbndlem1  27531  logdivbnd  27534  pntrlog2bndlem4  27558  pntibndlem2  27569  pntibndlem3  27570  pntlemh  27577  pntlemr  27580  pntlemk  27584  pntlemo  27585  ostth2lem1  27596  ostth2lem3  27613  ostth3  27616  axcontlem2  28848  nmoub3i  30655  blocni  30687  ubthlem3  30754  minvecolem2  30757  bcs2  31064  nmopub2tALT  31791  nmfnleub2  31808  nmophmi  31913  bdophmi  31914  lnconi  31915  cnlnadjlem2  31950  cnlnadjlem7  31955  nmopadjlem  31971  nmopcoadji  31983  leopnmid  32020  cdj1i  32315  cdj3lem2b  32319  cdj3i  32323  addltmulALT  32328  pnfinf  32983  rezh  33700  sgnmul  34290  sgnmulsgn  34297  sgnmulsgp  34298  signshf  34348  knoppndvlem15  36129  knoppndvlem21  36135  itg2addnclem  37272  ftc1anclem3  37296  isbnd2  37384  isbnd3  37385  equivbnd  37391  aks6d1c7lem1  41780  2xp3dxp2ge1d  41824  resubdi  42083  pellexlem5  42392  pell1234qrmulcl  42414  pellfundex  42445  rmspecsqrtnq  42465  jm2.24nn  42519  jm2.17a  42520  jm2.17b  42521  jm2.17c  42522  acongrep  42540  acongeq  42543  jm3.1lem2  42578  mulltgt0  44523  ltdiv23neg  44911  fmul01  45103  fmuldfeq  45106  fmul01lt1lem1  45107  fmul01lt1lem2  45108  stoweidlem3  45526  stoweidlem13  45536  stoweidlem17  45540  stoweidlem34  45557  stoweidlem42  45565  stoweidlem48  45571  fourierdlem83  45712  hoidmvlelem2  46119  smfmullem1  46314  2leaddle2  46813  itsclc0lem1  48012  amgmwlem  48418