Theorem remulcl 8007

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  (class class class)co 5922  ℝcr 7878   · cmul 7884

This theorem was proved from axioms:  ax-mulrcl 7978

This theorem is referenced by:  remulcli  8040  remulcld  8057  axmulgt0  8098  msqge0  8643  mulge0  8646  recexaplem2  8679  recexap  8680  ltmul12a  8887  lemul12b  8888  mulgt1  8890  ltdivmul  8903  cju  8988  addltmul  9228  zmulcl  9379  irrmul  9721  rpmulcl  9753  ge0mulcl  10057  iccdil  10073  reexpcl  10648  reexpclzap  10651  expge0  10667  expge1  10668  expubnd  10688  bernneq  10752  faclbnd  10833  faclbnd3  10835  facavg  10838  crre  11022  remim  11025  mulreap  11029  amgm2  11283  fprodrecl  11773  fprodreclf  11779  efcllemp  11823  ege2le3  11836  ef01bndlem  11921  cos01gt0  11928  4sqlem11  12570  dveflem  14962  sinq12gt0  15066  tangtx  15074  coskpi  15084  relogexp  15108  logcxp  15133  rpabscxpbnd  15176