Theorem remulcl 11209

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

Assertion

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

Proof of Theorem remulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  (class class class)co 7413  ℝcr 11123   · cmul 11129

This proof depends on axioms:  ax-mulrcl 11187

This theorem is used by:  1re  11232  remulcli  11249  remulcld  11263  axmulgt0  11308  00id  11409  mul02lem1  11410  recextlem2  11869  recex  11870  lemul1  12091  ltmul12a  12095  lemul12b  12096  mulgt1  12100  mulge0b  12109  mulle0b  12110  ltdivmul  12114  ledivmul  12115  lt2mul2div  12117  lemuldiv  12119  ltdiv23  12130  lediv23  12131  supmullem2  12210  cju  12238  addltmul  12504  zmulcl  12667  irrmul  13024  rpnnen1lem2  13027  rpnnen1lem1  13028  rpnnen1lem3  13029  rpnnen1lem5  13031  rpmulcl  13067  xmulasslem3  13338  xadddilem  13346  ge0mulcl  13514  iccdil  13543  mulmod0  13938  modmulnn  13950  modcyc  13967  modmul1  13988  modaddmulmod  14002  moddi  14003  addmodlteq  14010  reexpcl  14142  reexpclz  14146  expge0  14162  expge1  14163  expubnd  14242  bernneq  14293  expmulnbnd  14299  digit2  14300  digit1  14301  discr  14304  faclbnd  14354  faclbnd3  14356  faclbnd5  14362  facavg  14365  cshweqrep  14892  sgnmul  15180  sgnmulsgn  15182  crre  15201  remim  15204  mulre  15208  01sqrexlem6  15334  01sqrexlem7  15335  sqreulem  15447  amgm2  15457  o1mul  15702  caucvgrlem  15760  climcndslem2  15939  climcnds  15940  fprodrecl  16040  fprodreclf  16046  iprodrecl  16089  rerisefaccl  16104  refallfaccl  16105  efcllem  16163  ege2le3  16176  ef01bndlem  16272  cos01gt0  16279  modprm0  16897  prmreclem3  17010  4sqlem11  17047  resubdrg  21821  nmoco  24963  nghmco  24964  blcvx  25024  iihalf1  25159  iihalf2  25161  iimulcl  25165  pcoass  25252  tcphcphlem1  25463  csbren  25627  trirn  25628  minveclem2  25654  sca2rab  25740  uniioombllem5  25815  mbfmulc2lem  25875  i1fmul  25924  i1fmulclem  25930  i1fmulc  25931  dveflem  26206  cmvth  26218  dvivthlem1  26235  dvfsumle  26248  dvfsumlem2  26254  pilem2  26688  tangtx  26743  sinq12gt0  26745  coskpi  26760  cosne0  26766  efif1olem2  26780  efif1olem4  26782  relogexp  26833  logcxp  26906  rpcxpcl  26913  abscxpbnd  26990  ang180lem1  27046  atantan  27160  atanbndlem  27162  o1cxp  27211  divsqrtsumlem  27216  jensenlem2  27224  jensen  27225  zetacvg  27251  regamcl  27297  basellem1  27317  basellem4  27320  basellem9  27325  chtublem  27447  chtub  27448  logfaclbnd  27458  bpos1lem  27518  bposlem1  27520  bposlem2  27521  bposlem6  27525  bposlem7  27526  bposlem9  27528  lgseisen  27615  chebbnd1lem2  27706  chebbnd1lem3  27707  chto1ub  27712  rplogsumlem1  27720  dchrisumlem3  27727  dchrvmasumlem2  27734  dchrisum0lem1b  27751  dchrisum0lem1  27752  dchrisum0lem2  27754  mulog2sumlem1  27770  mulog2sumlem2  27771  log2sumbnd  27780  selberglem2  27782  chpdifbndlem1  27789  logdivbnd  27792  pntrlog2bndlem4  27816  pntibndlem2  27827  pntibndlem3  27828  pntlemh  27835  pntlemr  27838  pntlemk  27842  pntlemo  27843  ostth2lem1  27854  ostth2lem3  27871  ostth3  27874  axcontlem2  29422  nmoub3i  31254  blocni  31286  ubthlem3  31353  minvecolem2  31356  bcs2  31663  nmopub2tALT  32390  nmfnleub2  32407  nmophmi  32512  bdophmi  32513  lnconi  32514  cnlnadjlem2  32549  cnlnadjlem7  32554  nmopadjlem  32570  nmopcoadji  32582  leopnmid  32619  cdj1i  32914  cdj3lem2b  32918  cdj3i  32922  addltmulALT  32927  sgnmulsgp  33302  pnfinf  33623  rezh  34479  signshf  35096  knoppndvlem15  37223  knoppndvlem21  37229  itg2addnclem  38420  ftc1anclem3  38444  isbnd2  38533  isbnd3  38534  equivbnd  38540  aks6d1c7lem1  43046  resubdi  43271  pellexlem5  43674  pell1234qrmulcl  43696  pellfundex  43727  rmspecsqrtnq  43747  jm2.24nn  43800  jm2.17a  43801  jm2.17b  43802  jm2.17c  43803  acongrep  43821  acongeq  43824  jm3.1lem2  43859  mulltgt0  45856  ltdiv23neg  46223  fmul01  46410  fmuldfeq  46413  fmul01lt1lem1  46414  fmul01lt1lem2  46415  stoweidlem3  46831  stoweidlem13  46841  stoweidlem17  46845  stoweidlem34  46862  stoweidlem42  46870  stoweidlem48  46876  fourierdlem83  47017  hoidmvlelem2  47424  smfmullem1  47619  2leaddle2  48186  itsclc0lem1  49686  crosspaltd  50799  amgmwlem  50820