Theorem remulcl 10418

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2050  (class class class)co 6974  ℝcr 10332   · cmul 10338

This theorem was proved from axioms:  ax-mulrcl 10396

This theorem is referenced by:  1re  10437  remulcli  10454  remulcld  10468  axmulgt0  10513  00id  10613  mul02lem1  10614  recextlem2  11070  recex  11071  lemul1  11291  ltmul12a  11295  lemul12b  11296  mulgt1  11298  mulge0b  11309  mulle0b  11310  ltdivmul  11314  ledivmul  11315  lt2mul2div  11317  lemuldiv  11319  ltdiv23  11330  lediv23  11331  supmullem2  11411  cju  11433  addltmul  11681  zmulcl  11842  irrmul  12186  rpnnen1lem2  12189  rpnnen1lem1  12190  rpnnen1lem3  12191  rpnnen1lem5  12193  rpmulcl  12227  xmulasslem3  12493  xadddilem  12501  ge0mulcl  12663  iccdil  12690  mulmod0  13058  modmulnn  13070  modcyc  13087  modmul1  13105  modaddmulmod  13119  moddi  13120  addmodlteq  13127  reexpcl  13259  reexpclz  13262  expge0  13278  expge1  13279  expubnd  13354  bernneq  13403  expmulnbnd  13409  digit2  13410  digit1  13411  discr  13414  faclbnd  13463  faclbnd3  13465  faclbnd5  13471  facavg  13474  cshweqrep  14043  crre  14332  remim  14335  mulre  14339  sqrlem6  14466  sqrlem7  14467  sqreulem  14578  amgm2  14588  o1mul  14830  caucvgrlem  14888  climcndslem2  15063  climcnds  15064  fprodrecl  15165  fprodreclf  15171  iprodrecl  15214  rerisefaccl  15229  refallfaccl  15230  efcllem  15289  ege2le3  15301  ef01bndlem  15395  cos01gt0  15402  modprm0  15996  prmreclem3  16108  4sqlem11  16145  resubdrg  20466  nmoco  23061  nghmco  23062  blcvx  23121  iihalf1  23250  iihalf2  23252  iimulcl  23256  pcoass  23343  tcphcphlem1  23553  csbren  23717  trirn  23718  minveclem2  23744  sca2rab  23828  uniioombllem5  23903  mbfmulc2lem  23963  i1fmul  24012  i1fmulclem  24018  i1fmulc  24019  dveflem  24291  cmvth  24303  dvivthlem1  24320  dvfsumle  24333  dvfsumlem2  24339  pilem2  24755  tangtx  24806  sinq12gt0  24808  coskpi  24823  cosne0  24827  efif1olem2  24840  efif1olem4  24842  relogexp  24892  logcxp  24965  rpcxpcl  24972  abscxpbnd  25047  ang180lem1  25100  atantan  25214  atanbndlem  25216  o1cxp  25266  divsqrtsumlem  25271  jensenlem2  25279  jensen  25280  zetacvg  25306  regamcl  25352  basellem1  25372  basellem4  25375  basellem9  25380  chtublem  25501  chtub  25502  logfaclbnd  25512  bpos1lem  25572  bposlem1  25574  bposlem2  25575  bposlem6  25579  bposlem7  25580  bposlem9  25582  lgseisen  25669  chebbnd1lem2  25760  chebbnd1lem3  25761  chto1ub  25766  rplogsumlem1  25774  dchrisumlem3  25781  dchrvmasumlem2  25788  dchrisum0lem1b  25805  dchrisum0lem1  25806  dchrisum0lem2  25808  mulog2sumlem1  25824  mulog2sumlem2  25825  log2sumbnd  25834  selberglem2  25836  chpdifbndlem1  25843  logdivbnd  25846  pntrlog2bndlem4  25870  pntibndlem2  25881  pntibndlem3  25882  pntlemh  25889  pntlemr  25892  pntlemk  25896  pntlemo  25897  ostth2lem1  25908  ostth2lem3  25925  ostth3  25928  axcontlem2  26466  nmoub3i  28339  blocni  28371  ubthlem3  28439  minvecolem2  28442  bcs2  28750  nmopub2tALT  29479  nmfnleub2  29496  nmophmi  29601  bdophmi  29602  lnconi  29603  cnlnadjlem2  29638  cnlnadjlem7  29643  nmopadjlem  29659  nmopcoadji  29671  leopnmid  29708  cdj1i  30003  cdj3lem2b  30007  cdj3i  30011  addltmulALT  30016  pnfinf  30507  rezh  30885  sgnmul  31475  sgnmulsgn  31482  sgnmulsgp  31483  signshf  31535  knoppndvlem15  33414  knoppndvlem21  33420  itg2addnclem  34413  ftc1anclem3  34439  isbnd2  34532  isbnd3  34533  equivbnd  34539  resubdi  38686  pellexlem5  38855  pell1234qrmulcl  38877  pellfundex  38908  rmspecsqrtnq  38928  jm2.24nn  38981  jm2.17a  38982  jm2.17b  38983  jm2.17c  38984  acongrep  39002  acongeq  39005  jm3.1lem2  39040  mulltgt0  40727  ltdiv23neg  41121  fmul01  41317  fmuldfeq  41320  fmul01lt1lem1  41321  fmul01lt1lem2  41322  stoweidlem3  41744  stoweidlem13  41754  stoweidlem17  41758  stoweidlem34  41775  stoweidlem42  41783  stoweidlem48  41789  fourierdlem83  41930  hoidmvlelem2  42334  smfmullem1  42522  2leaddle2  42929  itsclc0lem1  44136  amgmwlem  44295