Theorem remulcl 11180

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094   · cmul 11100

This theorem was proved from axioms:  ax-mulrcl 11158

This theorem is referenced by:  1re  11203  remulcli  11220  remulcld  11234  axmulgt0  11279  00id  11380  mul02lem1  11381  recextlem2  11840  recex  11841  lemul1  12062  ltmul12a  12066  lemul12b  12067  mulgt1  12071  mulge0b  12080  mulle0b  12081  ltdivmul  12085  ledivmul  12086  lt2mul2div  12088  lemuldiv  12090  ltdiv23  12101  lediv23  12102  supmullem2  12181  cju  12209  addltmul  12475  zmulcl  12638  irrmul  12993  rpnnen1lem2  12996  rpnnen1lem1  12997  rpnnen1lem3  12998  rpnnen1lem5  13000  rpmulcl  13036  xmulasslem3  13307  xadddilem  13315  ge0mulcl  13483  iccdil  13512  mulmod0  13906  modmulnn  13918  modcyc  13935  modmul1  13956  modaddmulmod  13970  moddi  13971  addmodlteq  13978  reexpcl  14110  reexpclz  14114  expge0  14130  expge1  14131  expubnd  14210  bernneq  14261  expmulnbnd  14267  digit2  14268  digit1  14269  discr  14272  faclbnd  14322  faclbnd3  14324  faclbnd5  14330  facavg  14333  cshweqrep  14854  sgnmul  15140  sgnmulsgn  15142  crre  15161  remim  15164  mulre  15168  01sqrexlem6  15294  01sqrexlem7  15295  sqreulem  15407  amgm2  15417  o1mul  15662  caucvgrlem  15720  climcndslem2  15900  climcnds  15901  fprodrecl  16003  fprodreclf  16009  iprodrecl  16052  rerisefaccl  16067  refallfaccl  16068  efcllem  16126  ege2le3  16139  ef01bndlem  16235  cos01gt0  16242  modprm0  16860  prmreclem3  16973  4sqlem11  17010  resubdrg  21758  nmoco  24894  nghmco  24895  blcvx  24955  iihalf1  25090  iihalf2  25092  iimulcl  25096  pcoass  25183  tcphcphlem1  25394  csbren  25558  trirn  25559  minveclem2  25585  sca2rab  25671  uniioombllem5  25746  mbfmulc2lem  25806  i1fmul  25855  i1fmulclem  25861  i1fmulc  25862  dveflem  26138  cmvth  26150  dvivthlem1  26167  dvfsumle  26180  dvfsumlem2  26186  pilem2  26615  tangtx  26670  sinq12gt0  26672  coskpi  26688  cosne0  26694  efif1olem2  26708  efif1olem4  26710  relogexp  26761  logcxp  26834  rpcxpcl  26841  abscxpbnd  26918  ang180lem1  26974  atantan  27088  atanbndlem  27090  o1cxp  27139  divsqrtsumlem  27144  jensenlem2  27152  jensen  27153  zetacvg  27179  regamcl  27225  basellem1  27245  basellem4  27248  basellem9  27253  chtublem  27375  chtub  27376  logfaclbnd  27386  bpos1lem  27446  bposlem1  27448  bposlem2  27449  bposlem6  27453  bposlem7  27454  bposlem9  27456  lgseisen  27543  chebbnd1lem2  27634  chebbnd1lem3  27635  chto1ub  27640  rplogsumlem1  27648  dchrisumlem3  27655  dchrvmasumlem2  27662  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2  27682  mulog2sumlem1  27698  mulog2sumlem2  27699  log2sumbnd  27708  selberglem2  27710  chpdifbndlem1  27717  logdivbnd  27720  pntrlog2bndlem4  27744  pntibndlem2  27755  pntibndlem3  27756  pntlemh  27763  pntlemr  27766  pntlemk  27770  pntlemo  27771  ostth2lem1  27782  ostth2lem3  27799  ostth3  27802  axcontlem2  29315  nmoub3i  31125  blocni  31157  ubthlem3  31224  minvecolem2  31227  bcs2  31534  nmopub2tALT  32261  nmfnleub2  32278  nmophmi  32383  bdophmi  32384  lnconi  32385  cnlnadjlem2  32420  cnlnadjlem7  32425  nmopadjlem  32441  nmopcoadji  32453  leopnmid  32490  cdj1i  32785  cdj3lem2b  32789  cdj3i  32793  addltmulALT  32798  sgnmulsgp  33176  pnfinf  33503  rezh  34359  signshf  34975  knoppndvlem15  37115  knoppndvlem21  37121  itg2addnclem  38322  ftc1anclem3  38346  isbnd2  38434  isbnd3  38435  equivbnd  38441  aks6d1c7lem1  42947  resubdi  43157  pellexlem5  43560  pell1234qrmulcl  43582  pellfundex  43613  rmspecsqrtnq  43633  jm2.24nn  43686  jm2.17a  43687  jm2.17b  43688  jm2.17c  43689  acongrep  43707  acongeq  43710  jm3.1lem2  43745  mulltgt0  45742  ltdiv23neg  46109  fmul01  46296  fmuldfeq  46299  fmul01lt1lem1  46300  fmul01lt1lem2  46301  stoweidlem3  46717  stoweidlem13  46727  stoweidlem17  46731  stoweidlem34  46748  stoweidlem42  46756  stoweidlem48  46762  fourierdlem83  46903  hoidmvlelem2  47310  smfmullem1  47505  2leaddle2  48035  itsclc0lem1  49536  amgmwlem  50622