Theorem remulcl 8000

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  (class class class)co 5918  ℝcr 7871   · cmul 7877

This theorem was proved from axioms:  ax-mulrcl 7971

This theorem is referenced by:  remulcli  8033  remulcld  8050  axmulgt0  8091  msqge0  8635  mulge0  8638  recexaplem2  8671  recexap  8672  ltmul12a  8879  lemul12b  8880  mulgt1  8882  ltdivmul  8895  cju  8980  addltmul  9219  zmulcl  9370  irrmul  9712  rpmulcl  9744  ge0mulcl  10048  iccdil  10064  reexpcl  10627  reexpclzap  10630  expge0  10646  expge1  10647  expubnd  10667  bernneq  10731  faclbnd  10812  faclbnd3  10814  facavg  10817  crre  11001  remim  11004  mulreap  11008  amgm2  11262  fprodrecl  11751  fprodreclf  11757  efcllemp  11801  ege2le3  11814  ef01bndlem  11899  cos01gt0  11906  4sqlem11  12539  dveflem  14872  sinq12gt0  14965  tangtx  14973  coskpi  14983  relogexp  15007  logcxp  15032  rpabscxpbnd  15073