Theorem remulcl 11289

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

Assertion

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

Proof of Theorem remulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  (class class class)co 7421  ℝcr 11203   · cmul 11209

This proof depends on axioms:  ax-mulrcl 11267

This theorem is used by:  1re  11312  remulcli  11329  remulcld  11343  axmulgt0  11388  00id  11489  mul02lem1  11490  recextlem2  11951  recex  11952  lemul1  12173  ltmul12a  12177  lemul12b  12178  mulgt1  12182  mulge0b  12191  mulle0b  12192  ltdivmul  12196  ledivmul  12197  lt2mul2div  12199  lemuldiv  12201  ltdiv23  12212  lediv23  12213  supmullem2  12292  cju  12320  addltmul  12586  zmulcl  12749  irrmul  13106  rpnnen1lem2  13109  rpnnen1lem1  13110  rpnnen1lem3  13111  rpnnen1lem5  13113  rpmulcl  13149  xmulasslem3  13420  xadddilem  13428  ge0mulcl  13596  iccdil  13625  mulmod0  14021  modmulnn  14033  modcyc  14050  modmul1  14071  modaddmulmod  14085  moddi  14086  addmodlteq  14093  reexpcl  14225  reexpclz  14229  expge0  14245  expge1  14246  expubnd  14325  bernneq  14377  expmulnbnd  14383  digit2  14384  digit1  14385  discr  14388  faclbnd  14438  faclbnd3  14440  faclbnd5  14446  facavg  14449  cshweqrep  14977  sgnmul  15266  sgnmulsgn  15268  crre  15287  remim  15290  mulre  15294  01sqrexlem6  15420  01sqrexlem7  15421  sqreulem  15533  amgm2  15543  o1mul  15788  caucvgrlem  15846  climcndslem2  16025  climcnds  16026  fprodrecl  16126  fprodreclf  16132  iprodrecl  16175  rerisefaccl  16190  refallfaccl  16191  efcllem  16249  ege2le3  16262  ef01bndlem  16358  cos01gt0  16365  modprm0  16989  prmreclem3  17102  4sqlem11  17139  resubdrg  21920  nmoco  25062  nghmco  25063  blcvx  25123  iihalf1  25258  iihalf2  25260  iimulcl  25264  pcoass  25351  tcphcphlem1  25562  csbren  25726  trirn  25727  minveclem2  25753  sca2rab  25839  uniioombllem5  25914  mbfmulc2lem  25974  i1fmul  26023  i1fmulclem  26029  i1fmulc  26030  dveflem  26305  cmvth  26317  dvivthlem1  26334  dvfsumle  26347  dvfsumlem2  26353  pilem2  26785  tangtx  26840  sinq12gt0  26842  coskpi  26857  cosne0  26863  efif1olem2  26877  efif1olem4  26879  relogexp  26930  logcxp  27003  rpcxpcl  27010  abscxpbnd  27087  ang180lem1  27143  atantan  27257  atanbndlem  27259  o1cxp  27308  divsqrtsumlem  27313  jensenlem2  27321  jensen  27322  zetacvg  27348  regamcl  27394  basellem1  27414  basellem4  27417  basellem9  27422  chtublem  27544  chtub  27545  logfaclbnd  27555  bpos1lem  27615  bposlem1  27617  bposlem2  27618  bposlem6  27622  bposlem7  27623  bposlem9  27625  lgseisen  27712  chebbnd1lem2  27803  chebbnd1lem3  27804  chto1ub  27809  rplogsumlem1  27817  dchrisumlem3  27824  dchrvmasumlem2  27831  dchrisum0lem1b  27848  dchrisum0lem1  27849  dchrisum0lem2  27851  mulog2sumlem1  27867  mulog2sumlem2  27868  log2sumbnd  27877  selberglem2  27879  chpdifbndlem1  27886  logdivbnd  27889  pntrlog2bndlem4  27913  pntibndlem2  27924  pntibndlem3  27925  pntlemh  27932  pntlemr  27935  pntlemk  27939  pntlemo  27940  ostth2lem1  27951  ostth2lem3  27968  ostth3  27971  axcontlem2  29549  nmoub3i  31381  blocni  31413  ubthlem3  31480  minvecolem2  31483  bcs2  31790  nmopub2tALT  32517  nmfnleub2  32534  nmophmi  32639  bdophmi  32640  lnconi  32641  cnlnadjlem2  32676  cnlnadjlem7  32681  nmopadjlem  32697  nmopcoadji  32709  leopnmid  32746  cdj1i  33041  cdj3lem2b  33045  cdj3i  33049  addltmulALT  33096  sgnmulsgp  33470  pnfinf  33791  rezh  34648  signshf  35264  knoppndvlem15  37485  knoppndvlem21  37491  itg2addnclem  38683  ftc1anclem3  38707  isbnd2  38811  isbnd3  38812  equivbnd  38818  aks6d1c7lem1  43324  resubdi  43541  pellexlem5  43934  pell1234qrmulcl  43956  pellfundex  43987  rmspecsqrtnq  44007  jm2.24nn  44060  jm2.17a  44061  jm2.17b  44062  jm2.17c  44063  acongrep  44081  acongeq  44084  jm3.1lem2  44119  mulltgt0  46133  ltdiv23neg  46499  fmul01  46686  fmuldfeq  46689  fmul01lt1lem1  46690  fmul01lt1lem2  46691  stoweidlem3  47107  stoweidlem13  47117  stoweidlem17  47121  stoweidlem34  47138  stoweidlem42  47146  stoweidlem48  47152  fourierdlem83  47293  hoidmvlelem2  47700  smfmullem1  47895  2leaddle2  48462  itsclc0lem1  49962  crosspaltd  51135  amgmwlem  51156