Theorem remulcl 11129

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043   · cmul 11049

This theorem was proved from axioms:  ax-mulrcl 11107

This theorem is referenced by:  1re  11150  remulcli  11166  remulcld  11180  axmulgt0  11224  00id  11325  mul02lem1  11326  recextlem2  11785  recex  11786  lemul1  12010  ltmul12a  12014  lemul12b  12015  mulgt1OLD  12017  mulgt1  12020  mulge0b  12029  mulle0b  12030  ltdivmul  12034  ledivmul  12035  lt2mul2div  12037  lemuldiv  12039  ltdiv23  12050  lediv23  12051  supmullem2  12130  cju  12158  addltmul  12394  zmulcl  12558  irrmul  12909  rpnnen1lem2  12912  rpnnen1lem1  12913  rpnnen1lem3  12914  rpnnen1lem5  12916  rpmulcl  12952  xmulasslem3  13222  xadddilem  13230  ge0mulcl  13398  iccdil  13427  mulmod0  13815  modmulnn  13827  modcyc  13844  modmul1  13865  modaddmulmod  13879  moddi  13880  addmodlteq  13887  reexpcl  14019  reexpclz  14023  expge0  14039  expge1  14040  expubnd  14119  bernneq  14170  expmulnbnd  14176  digit2  14177  digit1  14178  discr  14181  faclbnd  14231  faclbnd3  14233  faclbnd5  14239  facavg  14242  cshweqrep  14762  crre  15056  remim  15059  mulre  15063  01sqrexlem6  15189  01sqrexlem7  15190  sqreulem  15302  amgm2  15312  o1mul  15557  caucvgrlem  15615  climcndslem2  15792  climcnds  15793  fprodrecl  15895  fprodreclf  15901  iprodrecl  15944  rerisefaccl  15959  refallfaccl  15960  efcllem  16019  ege2le3  16032  ef01bndlem  16128  cos01gt0  16135  modprm0  16752  prmreclem3  16865  4sqlem11  16902  resubdrg  21493  nmoco  24601  nghmco  24602  blcvx  24662  iihalf1  24801  iihalf2  24804  iimulcl  24809  pcoass  24900  tcphcphlem1  25111  csbren  25275  trirn  25276  minveclem2  25302  sca2rab  25389  uniioombllem5  25464  mbfmulc2lem  25524  i1fmul  25573  i1fmulclem  25579  i1fmulc  25580  dveflem  25859  cmvth  25871  cmvthOLD  25872  dvivthlem1  25889  dvfsumle  25902  dvfsumleOLD  25903  dvfsumlem2  25909  dvfsumlem2OLD  25910  pilem2  26338  tangtx  26390  sinq12gt0  26392  coskpi  26408  cosne0  26414  efif1olem2  26428  efif1olem4  26430  relogexp  26481  logcxp  26554  rpcxpcl  26561  abscxpbnd  26639  ang180lem1  26695  atantan  26809  atanbndlem  26811  o1cxp  26861  divsqrtsumlem  26866  jensenlem2  26874  jensen  26875  zetacvg  26901  regamcl  26947  basellem1  26967  basellem4  26970  basellem9  26975  chtublem  27098  chtub  27099  logfaclbnd  27109  bpos1lem  27169  bposlem1  27171  bposlem2  27172  bposlem6  27176  bposlem7  27177  bposlem9  27179  lgseisen  27266  chebbnd1lem2  27357  chebbnd1lem3  27358  chto1ub  27363  rplogsumlem1  27371  dchrisumlem3  27378  dchrvmasumlem2  27385  dchrisum0lem1b  27402  dchrisum0lem1  27403  dchrisum0lem2  27405  mulog2sumlem1  27421  mulog2sumlem2  27422  log2sumbnd  27431  selberglem2  27433  chpdifbndlem1  27440  logdivbnd  27443  pntrlog2bndlem4  27467  pntibndlem2  27478  pntibndlem3  27479  pntlemh  27486  pntlemr  27489  pntlemk  27493  pntlemo  27494  ostth2lem1  27505  ostth2lem3  27522  ostth3  27525  axcontlem2  28868  nmoub3i  30675  blocni  30707  ubthlem3  30774  minvecolem2  30777  bcs2  31084  nmopub2tALT  31811  nmfnleub2  31828  nmophmi  31933  bdophmi  31934  lnconi  31935  cnlnadjlem2  31970  cnlnadjlem7  31975  nmopadjlem  31991  nmopcoadji  32003  leopnmid  32040  cdj1i  32335  cdj3lem2b  32339  cdj3i  32343  addltmulALT  32348  sgnmul  32733  sgnmulsgn  32740  sgnmulsgp  32741  pnfinf  33110  rezh  33932  signshf  34552  knoppndvlem15  36487  knoppndvlem21  36493  itg2addnclem  37638  ftc1anclem3  37662  isbnd2  37750  isbnd3  37751  equivbnd  37757  aks6d1c7lem1  42141  resubdi  42357  pellexlem5  42794  pell1234qrmulcl  42816  pellfundex  42847  rmspecsqrtnq  42867  jm2.24nn  42921  jm2.17a  42922  jm2.17b  42923  jm2.17c  42924  acongrep  42942  acongeq  42945  jm3.1lem2  42980  mulltgt0  44989  ltdiv23neg  45363  fmul01  45551  fmuldfeq  45554  fmul01lt1lem1  45555  fmul01lt1lem2  45556  stoweidlem3  45974  stoweidlem13  45984  stoweidlem17  45988  stoweidlem34  46005  stoweidlem42  46013  stoweidlem48  46019  fourierdlem83  46160  hoidmvlelem2  46567  smfmullem1  46762  2leaddle2  47272  itsclc0lem1  48718  amgmwlem  49764