Theorem remulcl 11152

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  (class class class)co 7391  ℝcr 11066   · cmul 11072

This theorem was proved from axioms:  ax-mulrcl 11130

This theorem is referenced by:  1re  11175  remulcli  11192  remulcld  11206  axmulgt0  11251  00id  11352  mul02lem1  11353  recextlem2  11812  recex  11813  lemul1  12037  ltmul12a  12041  lemul12b  12042  mulgt1OLD  12044  mulgt1  12047  mulge0b  12056  mulle0b  12057  ltdivmul  12061  ledivmul  12062  lt2mul2div  12064  lemuldiv  12066  ltdiv23  12077  lediv23  12078  supmullem2  12157  cju  12185  addltmul  12451  zmulcl  12614  irrmul  12969  rpnnen1lem2  12972  rpnnen1lem1  12973  rpnnen1lem3  12974  rpnnen1lem5  12976  rpmulcl  13012  xmulasslem3  13283  xadddilem  13291  ge0mulcl  13459  iccdil  13488  mulmod0  13881  modmulnn  13893  modcyc  13910  modmul1  13931  modaddmulmod  13945  moddi  13946  addmodlteq  13953  reexpcl  14085  reexpclz  14089  expge0  14105  expge1  14106  expubnd  14185  bernneq  14236  expmulnbnd  14242  digit2  14243  digit1  14244  discr  14247  faclbnd  14297  faclbnd3  14299  faclbnd5  14305  facavg  14308  cshweqrep  14828  sgnmul  15111  sgnmulsgn  15113  crre  15132  remim  15135  mulre  15139  01sqrexlem6  15265  01sqrexlem7  15266  sqreulem  15378  amgm2  15388  o1mul  15633  caucvgrlem  15691  climcndslem2  15871  climcnds  15872  fprodrecl  15974  fprodreclf  15980  iprodrecl  16023  rerisefaccl  16038  refallfaccl  16039  efcllem  16098  ege2le3  16111  ef01bndlem  16207  cos01gt0  16214  modprm0  16832  prmreclem3  16945  4sqlem11  16982  resubdrg  21648  nmoco  24785  nghmco  24786  blcvx  24846  iihalf1  24981  iihalf2  24983  iimulcl  24987  pcoass  25074  tcphcphlem1  25285  csbren  25449  trirn  25450  minveclem2  25476  sca2rab  25562  uniioombllem5  25637  mbfmulc2lem  25697  i1fmul  25746  i1fmulclem  25752  i1fmulc  25753  dveflem  26029  cmvth  26041  dvivthlem1  26058  dvfsumle  26071  dvfsumlem2  26077  pilem2  26503  tangtx  26558  sinq12gt0  26560  coskpi  26576  cosne0  26582  efif1olem2  26596  efif1olem4  26598  relogexp  26649  logcxp  26722  rpcxpcl  26729  abscxpbnd  26806  ang180lem1  26862  atantan  26976  atanbndlem  26978  o1cxp  27027  divsqrtsumlem  27032  jensenlem2  27040  jensen  27041  zetacvg  27067  regamcl  27113  basellem1  27133  basellem4  27136  basellem9  27141  chtublem  27263  chtub  27264  logfaclbnd  27274  bpos1lem  27334  bposlem1  27336  bposlem2  27337  bposlem6  27341  bposlem7  27342  bposlem9  27344  lgseisen  27431  chebbnd1lem2  27522  chebbnd1lem3  27523  chto1ub  27528  rplogsumlem1  27536  dchrisumlem3  27543  dchrvmasumlem2  27550  dchrisum0lem1b  27567  dchrisum0lem1  27568  dchrisum0lem2  27570  mulog2sumlem1  27586  mulog2sumlem2  27587  log2sumbnd  27596  selberglem2  27598  chpdifbndlem1  27605  logdivbnd  27608  pntrlog2bndlem4  27632  pntibndlem2  27643  pntibndlem3  27644  pntlemh  27651  pntlemr  27654  pntlemk  27658  pntlemo  27659  ostth2lem1  27670  ostth2lem3  27687  ostth3  27690  axcontlem2  29123  nmoub3i  30933  blocni  30965  ubthlem3  31032  minvecolem2  31035  bcs2  31342  nmopub2tALT  32069  nmfnleub2  32086  nmophmi  32191  bdophmi  32192  lnconi  32193  cnlnadjlem2  32228  cnlnadjlem7  32233  nmopadjlem  32249  nmopcoadji  32261  leopnmid  32298  cdj1i  32593  cdj3lem2b  32597  cdj3i  32601  addltmulALT  32606  sgnmulsgp  32995  pnfinf  33324  rezh  34227  signshf  34843  knoppndvlem15  36925  knoppndvlem21  36931  itg2addnclem  38131  ftc1anclem3  38155  isbnd2  38243  isbnd3  38244  equivbnd  38250  aks6d1c7lem1  42758  resubdi  42966  pellexlem5  43371  pell1234qrmulcl  43393  pellfundex  43424  rmspecsqrtnq  43444  jm2.24nn  43497  jm2.17a  43498  jm2.17b  43499  jm2.17c  43500  acongrep  43518  acongeq  43521  jm3.1lem2  43556  mulltgt0  45563  ltdiv23neg  45930  fmul01  46117  fmuldfeq  46120  fmul01lt1lem1  46121  fmul01lt1lem2  46122  stoweidlem3  46538  stoweidlem13  46548  stoweidlem17  46552  stoweidlem34  46569  stoweidlem42  46577  stoweidlem48  46583  fourierdlem83  46724  hoidmvlelem2  47131  smfmullem1  47326  2leaddle2  47853  itsclc0lem1  49339  amgmwlem  50384