Theorem remulcl 7772

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1481  (class class class)co 5782  ℝcr 7643   · cmul 7649

This theorem was proved from axioms:  ax-mulrcl 7743

This theorem is referenced by:  remulcli  7804  remulcld  7820  axmulgt0  7860  msqge0  8402  mulge0  8405  recexaplem2  8437  recexap  8438  ltmul12a  8642  lemul12b  8643  mulgt1  8645  ltdivmul  8658  cju  8743  addltmul  8980  zmulcl  9131  irrmul  9466  rpmulcl  9495  ge0mulcl  9795  iccdil  9811  reexpcl  10341  reexpclzap  10344  expge0  10360  expge1  10361  expubnd  10381  bernneq  10443  faclbnd  10519  faclbnd3  10521  facavg  10524  crre  10661  remim  10664  mulreap  10668  amgm2  10922  efcllemp  11401  ege2le3  11414  ef01bndlem  11499  cos01gt0  11505  dveflem  12895  sinq12gt0  12959  tangtx  12967  coskpi  12977  relogexp  13001  logcxp  13026  rpabscxpbnd  13067