Theorem remulcl 11111

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  (class class class)co 7358  ℝcr 11025   · cmul 11031

This theorem was proved from axioms:  ax-mulrcl 11089

This theorem is referenced by:  1re  11132  remulcli  11148  remulcld  11162  axmulgt0  11207  00id  11308  mul02lem1  11309  recextlem2  11768  recex  11769  lemul1  11993  ltmul12a  11997  lemul12b  11998  mulgt1OLD  12000  mulgt1  12003  mulge0b  12012  mulle0b  12013  ltdivmul  12017  ledivmul  12018  lt2mul2div  12020  lemuldiv  12022  ltdiv23  12033  lediv23  12034  supmullem2  12113  cju  12141  addltmul  12377  zmulcl  12540  irrmul  12887  rpnnen1lem2  12890  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  rpmulcl  12930  xmulasslem3  13201  xadddilem  13209  ge0mulcl  13377  iccdil  13406  mulmod0  13797  modmulnn  13809  modcyc  13826  modmul1  13847  modaddmulmod  13861  moddi  13862  addmodlteq  13869  reexpcl  14001  reexpclz  14005  expge0  14021  expge1  14022  expubnd  14101  bernneq  14152  expmulnbnd  14158  digit2  14159  digit1  14160  discr  14163  faclbnd  14213  faclbnd3  14215  faclbnd5  14221  facavg  14224  cshweqrep  14744  crre  15037  remim  15040  mulre  15044  01sqrexlem6  15170  01sqrexlem7  15171  sqreulem  15283  amgm2  15293  o1mul  15538  caucvgrlem  15596  climcndslem2  15773  climcnds  15774  fprodrecl  15876  fprodreclf  15882  iprodrecl  15925  rerisefaccl  15940  refallfaccl  15941  efcllem  16000  ege2le3  16013  ef01bndlem  16109  cos01gt0  16116  modprm0  16733  prmreclem3  16846  4sqlem11  16883  resubdrg  21563  nmoco  24681  nghmco  24682  blcvx  24742  iihalf1  24881  iihalf2  24884  iimulcl  24889  pcoass  24980  tcphcphlem1  25191  csbren  25355  trirn  25356  minveclem2  25382  sca2rab  25469  uniioombllem5  25544  mbfmulc2lem  25604  i1fmul  25653  i1fmulclem  25659  i1fmulc  25660  dveflem  25939  cmvth  25951  cmvthOLD  25952  dvivthlem1  25969  dvfsumle  25982  dvfsumleOLD  25983  dvfsumlem2  25989  dvfsumlem2OLD  25990  pilem2  26418  tangtx  26470  sinq12gt0  26472  coskpi  26488  cosne0  26494  efif1olem2  26508  efif1olem4  26510  relogexp  26561  logcxp  26634  rpcxpcl  26641  abscxpbnd  26719  ang180lem1  26775  atantan  26889  atanbndlem  26891  o1cxp  26941  divsqrtsumlem  26946  jensenlem2  26954  jensen  26955  zetacvg  26981  regamcl  27027  basellem1  27047  basellem4  27050  basellem9  27055  chtublem  27178  chtub  27179  logfaclbnd  27189  bpos1lem  27249  bposlem1  27251  bposlem2  27252  bposlem6  27256  bposlem7  27257  bposlem9  27259  lgseisen  27346  chebbnd1lem2  27437  chebbnd1lem3  27438  chto1ub  27443  rplogsumlem1  27451  dchrisumlem3  27458  dchrvmasumlem2  27465  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2  27485  mulog2sumlem1  27501  mulog2sumlem2  27502  log2sumbnd  27511  selberglem2  27513  chpdifbndlem1  27520  logdivbnd  27523  pntrlog2bndlem4  27547  pntibndlem2  27558  pntibndlem3  27559  pntlemh  27566  pntlemr  27569  pntlemk  27573  pntlemo  27574  ostth2lem1  27585  ostth2lem3  27602  ostth3  27605  axcontlem2  29038  nmoub3i  30848  blocni  30880  ubthlem3  30947  minvecolem2  30950  bcs2  31257  nmopub2tALT  31984  nmfnleub2  32001  nmophmi  32106  bdophmi  32107  lnconi  32108  cnlnadjlem2  32143  cnlnadjlem7  32148  nmopadjlem  32164  nmopcoadji  32176  leopnmid  32213  cdj1i  32508  cdj3lem2b  32512  cdj3i  32516  addltmulALT  32521  sgnmul  32916  sgnmulsgn  32923  sgnmulsgp  32924  pnfinf  33265  rezh  34126  signshf  34745  knoppndvlem15  36726  knoppndvlem21  36732  itg2addnclem  37872  ftc1anclem3  37896  isbnd2  37984  isbnd3  37985  equivbnd  37991  aks6d1c7lem1  42434  resubdi  42651  pellexlem5  43075  pell1234qrmulcl  43097  pellfundex  43128  rmspecsqrtnq  43148  jm2.24nn  43201  jm2.17a  43202  jm2.17b  43203  jm2.17c  43204  acongrep  43222  acongeq  43225  jm3.1lem2  43260  mulltgt0  45267  ltdiv23neg  45638  fmul01  45826  fmuldfeq  45829  fmul01lt1lem1  45830  fmul01lt1lem2  45831  stoweidlem3  46247  stoweidlem13  46257  stoweidlem17  46261  stoweidlem34  46278  stoweidlem42  46286  stoweidlem48  46292  fourierdlem83  46433  hoidmvlelem2  46840  smfmullem1  47035  2leaddle2  47544  itsclc0lem1  49002  amgmwlem  50047