Theorem remulcl 7881

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2136  (class class class)co 5842  ℝcr 7752   · cmul 7758

This theorem was proved from axioms:  ax-mulrcl 7852

This theorem is referenced by:  remulcli  7913  remulcld  7929  axmulgt0  7970  msqge0  8514  mulge0  8517  recexaplem2  8549  recexap  8550  ltmul12a  8755  lemul12b  8756  mulgt1  8758  ltdivmul  8771  cju  8856  addltmul  9093  zmulcl  9244  irrmul  9585  rpmulcl  9614  ge0mulcl  9918  iccdil  9934  reexpcl  10472  reexpclzap  10475  expge0  10491  expge1  10492  expubnd  10512  bernneq  10575  faclbnd  10654  faclbnd3  10656  facavg  10659  crre  10799  remim  10802  mulreap  10806  amgm2  11060  fprodrecl  11549  fprodreclf  11555  efcllemp  11599  ege2le3  11612  ef01bndlem  11697  cos01gt0  11703  dveflem  13327  sinq12gt0  13391  tangtx  13399  coskpi  13409  relogexp  13433  logcxp  13458  rpabscxpbnd  13499