Theorem remulcl 11222

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  (class class class)co 7413  ℝcr 11136   · cmul 11142

This theorem was proved from axioms:  ax-mulrcl 11200

This theorem is referenced by:  1re  11243  remulcli  11259  remulcld  11273  axmulgt0  11317  00id  11418  mul02lem1  11419  recextlem2  11876  recex  11877  lemul1  12101  ltmul12a  12105  lemul12b  12106  mulgt1OLD  12108  mulgt1  12111  mulge0b  12120  mulle0b  12121  ltdivmul  12125  ledivmul  12126  lt2mul2div  12128  lemuldiv  12130  ltdiv23  12141  lediv23  12142  supmullem2  12221  cju  12244  addltmul  12485  zmulcl  12649  irrmul  12998  rpnnen1lem2  13001  rpnnen1lem1  13002  rpnnen1lem3  13003  rpnnen1lem5  13005  rpmulcl  13040  xmulasslem3  13310  xadddilem  13318  ge0mulcl  13483  iccdil  13512  mulmod0  13899  modmulnn  13911  modcyc  13928  modmul1  13947  modaddmulmod  13961  moddi  13962  addmodlteq  13969  reexpcl  14101  reexpclz  14105  expge0  14121  expge1  14122  expubnd  14199  bernneq  14250  expmulnbnd  14256  digit2  14257  digit1  14258  discr  14261  faclbnd  14311  faclbnd3  14313  faclbnd5  14319  facavg  14322  cshweqrep  14841  crre  15135  remim  15138  mulre  15142  01sqrexlem6  15268  01sqrexlem7  15269  sqreulem  15380  amgm2  15390  o1mul  15633  caucvgrlem  15691  climcndslem2  15868  climcnds  15869  fprodrecl  15971  fprodreclf  15977  iprodrecl  16020  rerisefaccl  16035  refallfaccl  16036  efcllem  16095  ege2le3  16108  ef01bndlem  16202  cos01gt0  16209  modprm0  16825  prmreclem3  16938  4sqlem11  16975  resubdrg  21580  nmoco  24694  nghmco  24695  blcvx  24755  iihalf1  24894  iihalf2  24897  iimulcl  24902  pcoass  24993  tcphcphlem1  25205  csbren  25369  trirn  25370  minveclem2  25396  sca2rab  25483  uniioombllem5  25558  mbfmulc2lem  25618  i1fmul  25667  i1fmulclem  25673  i1fmulc  25674  dveflem  25953  cmvth  25965  cmvthOLD  25966  dvivthlem1  25983  dvfsumle  25996  dvfsumleOLD  25997  dvfsumlem2  26003  dvfsumlem2OLD  26004  pilem2  26432  tangtx  26483  sinq12gt0  26485  coskpi  26501  cosne0  26507  efif1olem2  26521  efif1olem4  26523  relogexp  26574  logcxp  26647  rpcxpcl  26654  abscxpbnd  26732  ang180lem1  26788  atantan  26902  atanbndlem  26904  o1cxp  26954  divsqrtsumlem  26959  jensenlem2  26967  jensen  26968  zetacvg  26994  regamcl  27040  basellem1  27060  basellem4  27063  basellem9  27068  chtublem  27191  chtub  27192  logfaclbnd  27202  bpos1lem  27262  bposlem1  27264  bposlem2  27265  bposlem6  27269  bposlem7  27270  bposlem9  27272  lgseisen  27359  chebbnd1lem2  27450  chebbnd1lem3  27451  chto1ub  27456  rplogsumlem1  27464  dchrisumlem3  27471  dchrvmasumlem2  27478  dchrisum0lem1b  27495  dchrisum0lem1  27496  dchrisum0lem2  27498  mulog2sumlem1  27514  mulog2sumlem2  27515  log2sumbnd  27524  selberglem2  27526  chpdifbndlem1  27533  logdivbnd  27536  pntrlog2bndlem4  27560  pntibndlem2  27571  pntibndlem3  27572  pntlemh  27579  pntlemr  27582  pntlemk  27586  pntlemo  27587  ostth2lem1  27598  ostth2lem3  27615  ostth3  27618  axcontlem2  28910  nmoub3i  30720  blocni  30752  ubthlem3  30819  minvecolem2  30822  bcs2  31129  nmopub2tALT  31856  nmfnleub2  31873  nmophmi  31978  bdophmi  31979  lnconi  31980  cnlnadjlem2  32015  cnlnadjlem7  32020  nmopadjlem  32036  nmopcoadji  32048  leopnmid  32085  cdj1i  32380  cdj3lem2b  32384  cdj3i  32388  addltmulALT  32393  pnfinf  33129  rezh  33929  sgnmul  34504  sgnmulsgn  34511  sgnmulsgp  34512  signshf  34562  knoppndvlem15  36486  knoppndvlem21  36492  itg2addnclem  37637  ftc1anclem3  37661  isbnd2  37749  isbnd3  37750  equivbnd  37756  aks6d1c7lem1  42140  2xp3dxp2ge1d  42201  resubdi  42389  pellexlem5  42807  pell1234qrmulcl  42829  pellfundex  42860  rmspecsqrtnq  42880  jm2.24nn  42934  jm2.17a  42935  jm2.17b  42936  jm2.17c  42937  acongrep  42955  acongeq  42958  jm3.1lem2  42993  mulltgt0  44984  ltdiv23neg  45362  fmul01  45552  fmuldfeq  45555  fmul01lt1lem1  45556  fmul01lt1lem2  45557  stoweidlem3  45975  stoweidlem13  45985  stoweidlem17  45989  stoweidlem34  46006  stoweidlem42  46014  stoweidlem48  46020  fourierdlem83  46161  hoidmvlelem2  46568  smfmullem1  46763  2leaddle2  47268  itsclc0lem1  48635  amgmwlem  49329