Theorem remulcl 8035

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2175  (class class class)co 5934  ℝcr 7906   · cmul 7912

This theorem was proved from axioms:  ax-mulrcl 8006

This theorem is referenced by:  remulcli  8068  remulcld  8085  axmulgt0  8126  msqge0  8671  mulge0  8674  recexaplem2  8707  recexap  8708  ltmul12a  8915  lemul12b  8916  mulgt1  8918  ltdivmul  8931  cju  9016  addltmul  9256  zmulcl  9408  irrmul  9750  rpmulcl  9782  ge0mulcl  10086  iccdil  10102  reexpcl  10682  reexpclzap  10685  expge0  10701  expge1  10702  expubnd  10722  bernneq  10786  faclbnd  10867  faclbnd3  10869  facavg  10872  crre  11087  remim  11090  mulreap  11094  amgm2  11348  fprodrecl  11838  fprodreclf  11844  efcllemp  11888  ege2le3  11901  ef01bndlem  11986  cos01gt0  11993  4sqlem11  12643  dveflem  15116  sinq12gt0  15220  tangtx  15228  coskpi  15238  relogexp  15262  logcxp  15287  rpabscxpbnd  15330