Theorem remulcl 11181

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  (class class class)co 7408  ℝcr 11095   · cmul 11101

This theorem was proved from axioms:  ax-mulrcl 11159

This theorem is referenced by:  1re  11204  remulcli  11221  remulcld  11235  axmulgt0  11280  00id  11381  mul02lem1  11382  recextlem2  11841  recex  11842  lemul1  12063  ltmul12a  12067  lemul12b  12068  mulgt1  12072  mulge0b  12081  mulle0b  12082  ltdivmul  12086  ledivmul  12087  lt2mul2div  12089  lemuldiv  12091  ltdiv23  12102  lediv23  12103  supmullem2  12182  cju  12210  addltmul  12476  zmulcl  12639  irrmul  12994  rpnnen1lem2  12997  rpnnen1lem1  12998  rpnnen1lem3  12999  rpnnen1lem5  13001  rpmulcl  13037  xmulasslem3  13308  xadddilem  13316  ge0mulcl  13484  iccdil  13513  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  16127  ege2le3  16140  ef01bndlem  16236  cos01gt0  16243  modprm0  16861  prmreclem3  16974  4sqlem11  17011  resubdrg  21723  nmoco  24859  nghmco  24860  blcvx  24920  iihalf1  25055  iihalf2  25057  iimulcl  25061  pcoass  25148  tcphcphlem1  25359  csbren  25523  trirn  25524  minveclem2  25550  sca2rab  25636  uniioombllem5  25711  mbfmulc2lem  25771  i1fmul  25820  i1fmulclem  25826  i1fmulc  25827  dveflem  26103  cmvth  26115  dvivthlem1  26132  dvfsumle  26145  dvfsumlem2  26151  pilem2  26577  tangtx  26632  sinq12gt0  26634  coskpi  26650  cosne0  26656  efif1olem2  26670  efif1olem4  26672  relogexp  26723  logcxp  26796  rpcxpcl  26803  abscxpbnd  26880  ang180lem1  26936  atantan  27050  atanbndlem  27052  o1cxp  27101  divsqrtsumlem  27106  jensenlem2  27114  jensen  27115  zetacvg  27141  regamcl  27187  basellem1  27207  basellem4  27210  basellem9  27215  chtublem  27337  chtub  27338  logfaclbnd  27348  bpos1lem  27408  bposlem1  27410  bposlem2  27411  bposlem6  27415  bposlem7  27416  bposlem9  27418  lgseisen  27505  chebbnd1lem2  27596  chebbnd1lem3  27597  chto1ub  27602  rplogsumlem1  27610  dchrisumlem3  27617  dchrvmasumlem2  27624  dchrisum0lem1b  27641  dchrisum0lem1  27642  dchrisum0lem2  27644  mulog2sumlem1  27660  mulog2sumlem2  27661  log2sumbnd  27670  selberglem2  27672  chpdifbndlem1  27679  logdivbnd  27682  pntrlog2bndlem4  27706  pntibndlem2  27717  pntibndlem3  27718  pntlemh  27725  pntlemr  27728  pntlemk  27732  pntlemo  27733  ostth2lem1  27744  ostth2lem3  27761  ostth3  27764  axcontlem2  29252  nmoub3i  31062  blocni  31094  ubthlem3  31161  minvecolem2  31164  bcs2  31471  nmopub2tALT  32198  nmfnleub2  32215  nmophmi  32320  bdophmi  32321  lnconi  32322  cnlnadjlem2  32357  cnlnadjlem7  32362  nmopadjlem  32378  nmopcoadji  32390  leopnmid  32427  cdj1i  32722  cdj3lem2b  32726  cdj3i  32730  addltmulALT  32735  sgnmulsgp  33113  pnfinf  33440  rezh  34300  signshf  34916  knoppndvlem15  37000  knoppndvlem21  37006  itg2addnclem  38205  ftc1anclem3  38229  isbnd2  38317  isbnd3  38318  equivbnd  38324  aks6d1c7lem1  42832  resubdi  43042  pellexlem5  43447  pell1234qrmulcl  43469  pellfundex  43500  rmspecsqrtnq  43520  jm2.24nn  43573  jm2.17a  43574  jm2.17b  43575  jm2.17c  43576  acongrep  43594  acongeq  43597  jm3.1lem2  43632  mulltgt0  45629  ltdiv23neg  45996  fmul01  46183  fmuldfeq  46186  fmul01lt1lem1  46187  fmul01lt1lem2  46188  stoweidlem3  46604  stoweidlem13  46614  stoweidlem17  46618  stoweidlem34  46635  stoweidlem42  46643  stoweidlem48  46649  fourierdlem83  46790  hoidmvlelem2  47197  smfmullem1  47392  2leaddle2  47919  itsclc0lem1  49416  amgmwlem  50471