Theorem remulcl 11195

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  (class class class)co 7409  ℝcr 11109   · cmul 11115

This theorem was proved from axioms:  ax-mulrcl 11173

This theorem is referenced by:  1re  11214  remulcli  11230  remulcld  11244  axmulgt0  11288  00id  11389  mul02lem1  11390  recextlem2  11845  recex  11846  lemul1  12066  ltmul12a  12070  lemul12b  12071  mulgt1  12073  mulge0b  12084  mulle0b  12085  ltdivmul  12089  ledivmul  12090  lt2mul2div  12092  lemuldiv  12094  ltdiv23  12105  lediv23  12106  supmullem2  12185  cju  12208  addltmul  12448  zmulcl  12611  irrmul  12958  rpnnen1lem2  12961  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  rpmulcl  12997  xmulasslem3  13265  xadddilem  13273  ge0mulcl  13438  iccdil  13467  mulmod0  13842  modmulnn  13854  modcyc  13871  modmul1  13889  modaddmulmod  13903  moddi  13904  addmodlteq  13911  reexpcl  14044  reexpclz  14048  expge0  14064  expge1  14065  expubnd  14142  bernneq  14192  expmulnbnd  14198  digit2  14199  digit1  14200  discr  14203  faclbnd  14250  faclbnd3  14252  faclbnd5  14258  facavg  14261  cshweqrep  14771  crre  15061  remim  15064  mulre  15068  01sqrexlem6  15194  01sqrexlem7  15195  sqreulem  15306  amgm2  15316  o1mul  15559  caucvgrlem  15619  climcndslem2  15796  climcnds  15797  fprodrecl  15897  fprodreclf  15903  iprodrecl  15946  rerisefaccl  15961  refallfaccl  15962  efcllem  16021  ege2le3  16033  ef01bndlem  16127  cos01gt0  16134  modprm0  16738  prmreclem3  16851  4sqlem11  16888  resubdrg  21161  nmoco  24254  nghmco  24255  blcvx  24314  iihalf1  24447  iihalf2  24449  iimulcl  24453  pcoass  24540  tcphcphlem1  24752  csbren  24916  trirn  24917  minveclem2  24943  sca2rab  25029  uniioombllem5  25104  mbfmulc2lem  25164  i1fmul  25213  i1fmulclem  25220  i1fmulc  25221  dveflem  25496  cmvth  25508  dvivthlem1  25525  dvfsumle  25538  dvfsumlem2  25544  pilem2  25964  tangtx  26015  sinq12gt0  26017  coskpi  26032  cosne0  26038  efif1olem2  26052  efif1olem4  26054  relogexp  26104  logcxp  26177  rpcxpcl  26184  abscxpbnd  26261  ang180lem1  26314  atantan  26428  atanbndlem  26430  o1cxp  26479  divsqrtsumlem  26484  jensenlem2  26492  jensen  26493  zetacvg  26519  regamcl  26565  basellem1  26585  basellem4  26588  basellem9  26593  chtublem  26714  chtub  26715  logfaclbnd  26725  bpos1lem  26785  bposlem1  26787  bposlem2  26788  bposlem6  26792  bposlem7  26793  bposlem9  26795  lgseisen  26882  chebbnd1lem2  26973  chebbnd1lem3  26974  chto1ub  26979  rplogsumlem1  26987  dchrisumlem3  26994  dchrvmasumlem2  27001  dchrisum0lem1b  27018  dchrisum0lem1  27019  dchrisum0lem2  27021  mulog2sumlem1  27037  mulog2sumlem2  27038  log2sumbnd  27047  selberglem2  27049  chpdifbndlem1  27056  logdivbnd  27059  pntrlog2bndlem4  27083  pntibndlem2  27094  pntibndlem3  27095  pntlemh  27102  pntlemr  27105  pntlemk  27109  pntlemo  27110  ostth2lem1  27121  ostth2lem3  27138  ostth3  27141  axcontlem2  28254  nmoub3i  30057  blocni  30089  ubthlem3  30156  minvecolem2  30159  bcs2  30466  nmopub2tALT  31193  nmfnleub2  31210  nmophmi  31315  bdophmi  31316  lnconi  31317  cnlnadjlem2  31352  cnlnadjlem7  31357  nmopadjlem  31373  nmopcoadji  31385  leopnmid  31422  cdj1i  31717  cdj3lem2b  31721  cdj3i  31725  addltmulALT  31730  pnfinf  32360  rezh  32982  sgnmul  33572  sgnmulsgn  33579  sgnmulsgp  33580  signshf  33630  gg-cmvth  35212  gg-dvfsumle  35213  gg-dvfsumlem2  35214  knoppndvlem15  35450  knoppndvlem21  35456  itg2addnclem  36587  ftc1anclem3  36611  isbnd2  36699  isbnd3  36700  equivbnd  36706  2xp3dxp2ge1d  41070  resubdi  41317  pellexlem5  41619  pell1234qrmulcl  41641  pellfundex  41672  rmspecsqrtnq  41692  jm2.24nn  41746  jm2.17a  41747  jm2.17b  41748  jm2.17c  41749  acongrep  41767  acongeq  41770  jm3.1lem2  41805  mulltgt0  43754  ltdiv23neg  44152  fmul01  44344  fmuldfeq  44347  fmul01lt1lem1  44348  fmul01lt1lem2  44349  stoweidlem3  44767  stoweidlem13  44777  stoweidlem17  44781  stoweidlem34  44798  stoweidlem42  44806  stoweidlem48  44812  fourierdlem83  44953  hoidmvlelem2  45360  smfmullem1  45555  2leaddle2  46054  itsclc0lem1  47490  amgmwlem  47897