Theorem remulcl 10303

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 2158  (class class class)co 6871  ℝcr 10217   · cmul 10223

This theorem was proved from axioms:  ax-mulrcl 10281

This theorem is referenced by:  1re  10322  remulcli  10338  remulcld  10352  axmulgt0  10394  00id  10493  mul02lem1  10494  recextlem2  10940  recex  10941  lemul1  11157  ltmul12a  11161  lemul12b  11162  mulgt1  11164  mulge0b  11175  mulle0b  11176  ltdivmul  11180  ledivmul  11181  lt2mul2div  11183  lemuldiv  11185  ltdiv23  11196  lediv23  11197  supmullem2  11276  cju  11298  addltmul  11531  zmulcl  11688  irrmul  12028  rpnnen1lem2  12029  rpnnen1lem1  12030  rpnnen1lem3  12031  rpnnen1lem5  12033  rpmulcl  12065  xmulasslem3  12330  xadddilem  12338  ge0mulcl  12501  iccdil  12529  mulmod0  12896  modmulnn  12908  modcyc  12925  modmul1  12943  modaddmulmod  12957  moddi  12958  addmodlteq  12965  reexpcl  13096  reexpclz  13099  expge0  13115  expge1  13116  expubnd  13140  bernneq  13209  expmulnbnd  13215  digit2  13216  digit1  13217  discr  13220  faclbnd  13293  faclbnd3  13295  faclbnd5  13301  facavg  13304  cshweqrep  13787  crre  14073  remim  14076  mulre  14080  sqrlem6  14207  sqrlem7  14208  sqreulem  14318  amgm2  14328  o1mul  14564  caucvgrlem  14622  climcndslem2  14800  climcnds  14801  fprodrecl  14900  fprodreclf  14906  iprodrecl  14949  rerisefaccl  14964  refallfaccl  14965  efcllem  15024  ege2le3  15036  ef01bndlem  15130  cos01gt0  15137  modprm0  15723  prmreclem3  15835  4sqlem11  15872  resubdrg  20159  nmoco  22750  nghmco  22751  blcvx  22810  iihalf1  22939  iihalf2  22941  iimulcl  22945  pcoass  23032  tchcphlem1  23242  csbren  23390  trirn  23391  minveclem2  23405  sca2rab  23489  uniioombllem5  23564  mbfmulc2lem  23624  i1fmul  23673  i1fmulclem  23679  i1fmulc  23680  dveflem  23952  cmvth  23964  dvivthlem1  23981  dvfsumle  23994  dvfsumlem2  24000  pilem2  24416  tangtx  24468  sinq12gt0  24470  coskpi  24483  cosne0  24487  efif1olem2  24500  efif1olem4  24502  relogexp  24552  logcxp  24625  rpcxpcl  24632  abscxpbnd  24704  ang180lem1  24749  atantan  24860  atanbndlem  24862  o1cxp  24911  divsqrtsumlem  24916  jensenlem2  24924  jensen  24925  zetacvg  24951  regamcl  24997  basellem1  25017  basellem4  25020  basellem9  25025  chtublem  25146  chtub  25147  logfaclbnd  25157  bpos1lem  25217  bposlem1  25219  bposlem2  25220  bposlem6  25224  bposlem7  25225  bposlem9  25227  lgseisen  25314  chebbnd1lem2  25369  chebbnd1lem3  25370  chto1ub  25375  rplogsumlem1  25383  dchrisumlem3  25390  dchrvmasumlem2  25397  dchrisum0lem1b  25414  dchrisum0lem1  25415  dchrisum0lem2  25417  mulog2sumlem1  25433  mulog2sumlem2  25434  log2sumbnd  25443  selberglem2  25445  chpdifbndlem1  25452  logdivbnd  25455  pntrlog2bndlem4  25479  pntibndlem2  25490  pntibndlem3  25491  pntlemh  25498  pntlemr  25501  pntlemk  25505  pntlemo  25506  ostth2lem1  25517  ostth2lem3  25534  ostth3  25537  axcontlem2  26055  nmoub3i  27953  blocni  27985  ubthlem3  28053  minvecolem2  28056  bcs2  28364  nmopub2tALT  29093  nmfnleub2  29110  nmophmi  29215  bdophmi  29216  lnconi  29217  cnlnadjlem2  29252  cnlnadjlem7  29257  nmopadjlem  29273  nmopcoadji  29285  leopnmid  29322  cdj1i  29617  cdj3lem2b  29621  cdj3i  29625  addltmulALT  29630  pnfinf  30059  rezh  30337  sgnmul  30926  sgnmulsgn  30933  sgnmulsgp  30934  signshf  30987  knoppndvlem15  32831  knoppndvlem21  32837  itg2addnclem  33770  ftc1anclem3  33796  isbnd2  33890  isbnd3  33891  equivbnd  33897  pellexlem5  37896  pell1234qrmulcl  37918  pellfundex  37949  rmspecsqrtnq  37969  jm2.24nn  38024  jm2.17a  38025  jm2.17b  38026  jm2.17c  38027  acongrep  38045  acongeq  38048  jm3.1lem2  38083  mulltgt0  39672  ltdiv23neg  40093  fmul01  40289  fmuldfeq  40292  fmul01lt1lem1  40293  fmul01lt1lem2  40294  stoweidlem3  40696  stoweidlem13  40706  stoweidlem17  40710  stoweidlem34  40727  stoweidlem42  40735  stoweidlem48  40741  fourierdlem83  40882  hoidmvlelem2  41289  smfmullem1  41477  2leaddle2  41885  amgmwlem  43116