Theorem remulcl 8307

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

Assertion

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

Proof of Theorem remulcl

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

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

This proof depends on axioms:  ax-mulrcl 8278

This theorem is used by:  remulcli  8340  remulcld  8356  axmulgt0  8397  msqge0  8944  mulge0  8947  recexaplem2  8980  recexap  8981  ltmul12a  9190  lemul12b  9191  mulgt1  9193  ltdivmul  9206  cju  9291  addltmul  9542  zmulcl  9698  irrmul  10047  rpmulcl  10079  ge0mulcl  10384  iccdil  10400  reexpcl  10993  reexpclzap  10996  expge0  11012  expge1  11013  expubnd  11033  bernneq  11098  faclbnd  11179  faclbnd3  11181  facavg  11184  crre  11622  remim  11625  mulreap  11629  amgm2  11884  fprodrecl  12375  fprodreclf  12381  efcllemp  12425  ege2le3  12438  ef01bndlem  12523  cos01gt0  12530  4sqlem11  13180  dveflem  15827  sinq12gt0  15931  tangtx  15939  coskpi  15949  relogexp  15973  logfac  15995  logcxp  15999  rpabscxpbnd  16042