Theorem remulcl 9900

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  (class class class)co 6549  ℝcr 9814   · cmul 9820

This theorem was proved from axioms:  ax-mulrcl 9878

This theorem is referenced by:  1re  9918  remulcli  9933  remulcld  9949  axmulgt0  9991  00id  10090  mul02lem1  10091  recextlem2  10537  recex  10538  lemul1  10754  ltmul12a  10758  lemul12b  10759  mulgt1  10761  mulge0b  10772  mulle0b  10773  ltdivmul  10777  ledivmul  10778  lt2mul2div  10780  lemuldiv  10782  ltdiv23  10793  lediv23  10794  supmullem2  10871  cju  10893  addltmul  11145  zmulcl  11303  irrmul  11689  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  rpmulcl  11731  xmulasslem3  11988  xadddilem  11996  ge0mulcl  12156  iccdil  12181  mulmod0  12538  modmulnn  12550  modcyc  12567  modmul1  12585  modaddmulmod  12599  moddi  12600  addmodlteq  12607  reexpcl  12739  reexpclz  12742  expge0  12758  expge1  12759  expubnd  12783  bernneq  12852  expmulnbnd  12858  digit2  12859  digit1  12860  discr  12863  faclbnd  12939  faclbnd3  12941  faclbnd5  12947  facavg  12950  cshweqrep  13418  crre  13702  remim  13705  mulre  13709  sqrlem6  13836  sqrlem7  13837  sqreulem  13947  amgm2  13957  o1mul  14193  caucvgrlem  14251  climcndslem2  14421  climcnds  14422  fprodrecl  14522  fprodreclf  14528  iprodrecl  14572  rerisefaccl  14587  refallfaccl  14588  efcllem  14647  ege2le3  14659  ef01bndlem  14753  cos01gt0  14760  modprm0  15348  prmreclem3  15460  4sqlem11  15497  resubdrg  19773  nmoco  22351  nghmco  22352  blcvx  22409  iihalf1  22538  iihalf2  22540  iimulcl  22544  pcoass  22632  tchcphlem1  22842  csbren  22990  trirn  22991  minveclem2  23005  sca2rab  23087  uniioombllem5  23161  mbfmulc2lem  23220  i1fmul  23269  i1fmulclem  23275  i1fmulc  23276  dveflem  23546  cmvth  23558  dvivthlem1  23575  dvfsumle  23588  dvfsumlem2  23594  pilem2  24010  tangtx  24061  sinq12gt0  24063  coskpi  24076  cosne0  24080  efif1olem2  24093  efif1olem4  24095  relogexp  24146  logcxp  24215  rpcxpcl  24222  abscxpbnd  24294  ang180lem1  24339  atantan  24450  atanbndlem  24452  o1cxp  24501  divsqrtsumlem  24506  jensenlem2  24514  jensen  24515  zetacvg  24541  regamcl  24587  basellem1  24607  basellem4  24610  basellem9  24615  chtublem  24736  chtub  24737  logfaclbnd  24747  bpos1lem  24807  bposlem1  24809  bposlem2  24810  bposlem6  24814  bposlem7  24815  bposlem9  24817  lgseisen  24904  chebbnd1lem2  24959  chebbnd1lem3  24960  chto1ub  24965  rplogsumlem1  24973  dchrisumlem3  24980  dchrvmasumlem2  24987  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2  25007  mulog2sumlem1  25023  mulog2sumlem2  25024  log2sumbnd  25033  selberglem2  25035  chpdifbndlem1  25042  logdivbnd  25045  pntrlog2bndlem4  25069  pntibndlem2  25080  pntibndlem3  25081  pntlemh  25088  pntlemr  25091  pntlemk  25095  pntlemo  25096  ostth2lem1  25107  ostth2lem3  25124  ostth3  25127  axcontlem2  25645  nmoub3i  27012  blocni  27044  ubthlem3  27112  minvecolem2  27115  bcs2  27423  nmopub2tALT  28152  nmfnleub2  28169  nmophmi  28274  bdophmi  28275  lnconi  28276  cnlnadjlem2  28311  cnlnadjlem7  28316  nmopadjlem  28332  nmopcoadji  28344  leopnmid  28381  cdj1i  28676  cdj3lem2b  28680  cdj3i  28684  addltmulALT  28689  pnfinf  29068  rezh  29343  sgnmul  29931  sgnmulsgn  29938  sgnmulsgp  29939  signshf  29991  knoppndvlem15  31687  knoppndvlem21  31693  itg2addnclem  32631  ftc1anclem3  32657  isbnd2  32752  isbnd3  32753  equivbnd  32759  pellexlem5  36415  pell1234qrmulcl  36437  pellfundex  36468  rmspecsqrtnq  36488  rmspecsqrtnqOLD  36489  jm2.24nn  36544  jm2.17a  36545  jm2.17b  36546  jm2.17c  36547  acongrep  36565  acongeq  36568  jm3.1lem2  36603  mulltgt0  38204  ltdiv23neg  38558  fmul01  38647  fmuldfeq  38650  fmul01lt1lem1  38651  fmul01lt1lem2  38652  stoweidlem3  38896  stoweidlem13  38906  stoweidlem17  38910  stoweidlem34  38927  stoweidlem42  38935  stoweidlem48  38941  fourierdlem83  39082  hoidmvlelem2  39486  smfmullem1  39676  2leaddle2  40344  amgmwlem  42357