Theorem remulcl 8308

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

Assertion

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

Proof of Theorem remulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  (class class class)co 6085  ℝcr 8179   · cmul 8185

This proof depends on axioms:  ax-mulrcl 8279

This theorem is used by:  remulcli  8341  remulcld  8357  axmulgt0  8398  msqge0  8947  mulge0  8950  recexaplem2  8983  recexap  8984  ltmul12a  9193  lemul12b  9194  mulgt1  9196  ltdivmul  9209  cju  9294  addltmul  9547  zmulcl  9703  irrmul  10058  rpmulcl  10090  ge0mulcl  10395  iccdil  10411  reexpcl  11008  reexpclzap  11011  expge0  11027  expge1  11028  expubnd  11048  bernneq  11113  faclbnd  11195  faclbnd3  11197  facavg  11200  crre  11638  remim  11641  mulreap  11645  amgm2  11901  fprodrecl  12394  fprodreclf  12400  efcllemp  12444  ege2le3  12457  ef01bndlem  12542  cos01gt0  12549  4sqlem11  13203  dveflem  15918  sinq12gt0  16023  tangtx  16031  coskpi  16041  relogexp  16066  logfac  16090  logcxp  16094  rpabscxpbnd  16137  chtublem  16256  chtqub  16257  bpos1lem  16270  bposlem1  16272  bposlem2  16273  bposlem6  16277  bposlem7  16278  bposlem9  16280