Theorem remulcl 11114

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  (class class class)co 7360  ℝcr 11028   · cmul 11034

This theorem was proved from axioms:  ax-mulrcl 11092

This theorem is referenced by:  1re  11135  remulcli  11152  remulcld  11166  axmulgt0  11211  00id  11312  mul02lem1  11313  recextlem2  11772  recex  11773  lemul1  11998  ltmul12a  12002  lemul12b  12003  mulgt1OLD  12005  mulgt1  12008  mulge0b  12017  mulle0b  12018  ltdivmul  12022  ledivmul  12023  lt2mul2div  12025  lemuldiv  12027  ltdiv23  12038  lediv23  12039  supmullem2  12118  cju  12146  addltmul  12404  zmulcl  12567  irrmul  12915  rpnnen1lem2  12918  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  rpmulcl  12958  xmulasslem3  13229  xadddilem  13237  ge0mulcl  13405  iccdil  13434  mulmod0  13827  modmulnn  13839  modcyc  13856  modmul1  13877  modaddmulmod  13891  moddi  13892  addmodlteq  13899  reexpcl  14031  reexpclz  14035  expge0  14051  expge1  14052  expubnd  14131  bernneq  14182  expmulnbnd  14188  digit2  14189  digit1  14190  discr  14193  faclbnd  14243  faclbnd3  14245  faclbnd5  14251  facavg  14254  cshweqrep  14774  crre  15067  remim  15070  mulre  15074  01sqrexlem6  15200  01sqrexlem7  15201  sqreulem  15313  amgm2  15323  o1mul  15568  caucvgrlem  15626  climcndslem2  15806  climcnds  15807  fprodrecl  15909  fprodreclf  15915  iprodrecl  15958  rerisefaccl  15973  refallfaccl  15974  efcllem  16033  ege2le3  16046  ef01bndlem  16142  cos01gt0  16149  modprm0  16767  prmreclem3  16880  4sqlem11  16917  resubdrg  21598  nmoco  24712  nghmco  24713  blcvx  24773  iihalf1  24908  iihalf2  24910  iimulcl  24914  pcoass  25001  tcphcphlem1  25212  csbren  25376  trirn  25377  minveclem2  25403  sca2rab  25489  uniioombllem5  25564  mbfmulc2lem  25624  i1fmul  25673  i1fmulclem  25679  i1fmulc  25680  dveflem  25956  cmvth  25968  dvivthlem1  25985  dvfsumle  25998  dvfsumlem2  26004  pilem2  26430  tangtx  26482  sinq12gt0  26484  coskpi  26500  cosne0  26506  efif1olem2  26520  efif1olem4  26522  relogexp  26573  logcxp  26646  rpcxpcl  26653  abscxpbnd  26730  ang180lem1  26786  atantan  26900  atanbndlem  26902  o1cxp  26952  divsqrtsumlem  26957  jensenlem2  26965  jensen  26966  zetacvg  26992  regamcl  27038  basellem1  27058  basellem4  27061  basellem9  27066  chtublem  27188  chtub  27189  logfaclbnd  27199  bpos1lem  27259  bposlem1  27261  bposlem2  27262  bposlem6  27266  bposlem7  27267  bposlem9  27269  lgseisen  27356  chebbnd1lem2  27447  chebbnd1lem3  27448  chto1ub  27453  rplogsumlem1  27461  dchrisumlem3  27468  dchrvmasumlem2  27475  dchrisum0lem1b  27492  dchrisum0lem1  27493  dchrisum0lem2  27495  mulog2sumlem1  27511  mulog2sumlem2  27512  log2sumbnd  27521  selberglem2  27523  chpdifbndlem1  27530  logdivbnd  27533  pntrlog2bndlem4  27557  pntibndlem2  27568  pntibndlem3  27569  pntlemh  27576  pntlemr  27579  pntlemk  27583  pntlemo  27584  ostth2lem1  27595  ostth2lem3  27612  ostth3  27615  axcontlem2  29048  nmoub3i  30859  blocni  30891  ubthlem3  30958  minvecolem2  30961  bcs2  31268  nmopub2tALT  31995  nmfnleub2  32012  nmophmi  32117  bdophmi  32118  lnconi  32119  cnlnadjlem2  32154  cnlnadjlem7  32159  nmopadjlem  32175  nmopcoadji  32187  leopnmid  32224  cdj1i  32519  cdj3lem2b  32523  cdj3i  32527  addltmulALT  32532  sgnmul  32923  sgnmulsgn  32930  sgnmulsgp  32931  pnfinf  33259  rezh  34129  signshf  34748  knoppndvlem15  36802  knoppndvlem21  36808  itg2addnclem  38006  ftc1anclem3  38030  isbnd2  38118  isbnd3  38119  equivbnd  38125  aks6d1c7lem1  42633  resubdi  42842  pellexlem5  43279  pell1234qrmulcl  43301  pellfundex  43332  rmspecsqrtnq  43352  jm2.24nn  43405  jm2.17a  43406  jm2.17b  43407  jm2.17c  43408  acongrep  43426  acongeq  43429  jm3.1lem2  43464  mulltgt0  45471  ltdiv23neg  45841  fmul01  46028  fmuldfeq  46031  fmul01lt1lem1  46032  fmul01lt1lem2  46033  stoweidlem3  46449  stoweidlem13  46459  stoweidlem17  46463  stoweidlem34  46480  stoweidlem42  46488  stoweidlem48  46494  fourierdlem83  46635  hoidmvlelem2  47042  smfmullem1  47237  2leaddle2  47758  itsclc0lem1  49244  amgmwlem  50289