Theorem remulcl 11113

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7353  ℝcr 11027   · cmul 11033

This theorem was proved from axioms:  ax-mulrcl 11091

This theorem is referenced by:  1re  11134  remulcli  11150  remulcld  11164  axmulgt0  11209  00id  11310  mul02lem1  11311  recextlem2  11770  recex  11771  lemul1  11995  ltmul12a  11999  lemul12b  12000  mulgt1OLD  12002  mulgt1  12005  mulge0b  12014  mulle0b  12015  ltdivmul  12019  ledivmul  12020  lt2mul2div  12022  lemuldiv  12024  ltdiv23  12035  lediv23  12036  supmullem2  12115  cju  12143  addltmul  12379  zmulcl  12543  irrmul  12894  rpnnen1lem2  12897  rpnnen1lem1  12898  rpnnen1lem3  12899  rpnnen1lem5  12901  rpmulcl  12937  xmulasslem3  13207  xadddilem  13215  ge0mulcl  13383  iccdil  13412  mulmod0  13800  modmulnn  13812  modcyc  13829  modmul1  13850  modaddmulmod  13864  moddi  13865  addmodlteq  13872  reexpcl  14004  reexpclz  14008  expge0  14024  expge1  14025  expubnd  14104  bernneq  14155  expmulnbnd  14161  digit2  14162  digit1  14163  discr  14166  faclbnd  14216  faclbnd3  14218  faclbnd5  14224  facavg  14227  cshweqrep  14746  crre  15040  remim  15043  mulre  15047  01sqrexlem6  15173  01sqrexlem7  15174  sqreulem  15286  amgm2  15296  o1mul  15541  caucvgrlem  15599  climcndslem2  15776  climcnds  15777  fprodrecl  15879  fprodreclf  15885  iprodrecl  15928  rerisefaccl  15943  refallfaccl  15944  efcllem  16003  ege2le3  16016  ef01bndlem  16112  cos01gt0  16119  modprm0  16736  prmreclem3  16849  4sqlem11  16886  resubdrg  21534  nmoco  24642  nghmco  24643  blcvx  24703  iihalf1  24842  iihalf2  24845  iimulcl  24850  pcoass  24941  tcphcphlem1  25152  csbren  25316  trirn  25317  minveclem2  25343  sca2rab  25430  uniioombllem5  25505  mbfmulc2lem  25565  i1fmul  25614  i1fmulclem  25620  i1fmulc  25621  dveflem  25900  cmvth  25912  cmvthOLD  25913  dvivthlem1  25930  dvfsumle  25943  dvfsumleOLD  25944  dvfsumlem2  25950  dvfsumlem2OLD  25951  pilem2  26379  tangtx  26431  sinq12gt0  26433  coskpi  26449  cosne0  26455  efif1olem2  26469  efif1olem4  26471  relogexp  26522  logcxp  26595  rpcxpcl  26602  abscxpbnd  26680  ang180lem1  26736  atantan  26850  atanbndlem  26852  o1cxp  26902  divsqrtsumlem  26907  jensenlem2  26915  jensen  26916  zetacvg  26942  regamcl  26988  basellem1  27008  basellem4  27011  basellem9  27016  chtublem  27139  chtub  27140  logfaclbnd  27150  bpos1lem  27210  bposlem1  27212  bposlem2  27213  bposlem6  27217  bposlem7  27218  bposlem9  27220  lgseisen  27307  chebbnd1lem2  27398  chebbnd1lem3  27399  chto1ub  27404  rplogsumlem1  27412  dchrisumlem3  27419  dchrvmasumlem2  27426  dchrisum0lem1b  27443  dchrisum0lem1  27444  dchrisum0lem2  27446  mulog2sumlem1  27462  mulog2sumlem2  27463  log2sumbnd  27472  selberglem2  27474  chpdifbndlem1  27481  logdivbnd  27484  pntrlog2bndlem4  27508  pntibndlem2  27519  pntibndlem3  27520  pntlemh  27527  pntlemr  27530  pntlemk  27534  pntlemo  27535  ostth2lem1  27546  ostth2lem3  27563  ostth3  27566  axcontlem2  28929  nmoub3i  30736  blocni  30768  ubthlem3  30835  minvecolem2  30838  bcs2  31145  nmopub2tALT  31872  nmfnleub2  31889  nmophmi  31994  bdophmi  31995  lnconi  31996  cnlnadjlem2  32031  cnlnadjlem7  32036  nmopadjlem  32052  nmopcoadji  32064  leopnmid  32101  cdj1i  32396  cdj3lem2b  32400  cdj3i  32404  addltmulALT  32409  sgnmul  32799  sgnmulsgn  32806  sgnmulsgp  32807  pnfinf  33144  rezh  33955  signshf  34575  knoppndvlem15  36519  knoppndvlem21  36525  itg2addnclem  37670  ftc1anclem3  37694  isbnd2  37782  isbnd3  37783  equivbnd  37789  aks6d1c7lem1  42173  resubdi  42389  pellexlem5  42826  pell1234qrmulcl  42848  pellfundex  42879  rmspecsqrtnq  42899  jm2.24nn  42952  jm2.17a  42953  jm2.17b  42954  jm2.17c  42955  acongrep  42973  acongeq  42976  jm3.1lem2  43011  mulltgt0  45020  ltdiv23neg  45393  fmul01  45581  fmuldfeq  45584  fmul01lt1lem1  45585  fmul01lt1lem2  45586  stoweidlem3  46004  stoweidlem13  46014  stoweidlem17  46018  stoweidlem34  46035  stoweidlem42  46043  stoweidlem48  46049  fourierdlem83  46190  hoidmvlelem2  46597  smfmullem1  46792  2leaddle2  47302  itsclc0lem1  48761  amgmwlem  49807