Theorem remulcl 8024

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  (class class class)co 5925  ℝcr 7895   · cmul 7901

This theorem was proved from axioms:  ax-mulrcl 7995

This theorem is referenced by:  remulcli  8057  remulcld  8074  axmulgt0  8115  msqge0  8660  mulge0  8663  recexaplem2  8696  recexap  8697  ltmul12a  8904  lemul12b  8905  mulgt1  8907  ltdivmul  8920  cju  9005  addltmul  9245  zmulcl  9396  irrmul  9738  rpmulcl  9770  ge0mulcl  10074  iccdil  10090  reexpcl  10665  reexpclzap  10668  expge0  10684  expge1  10685  expubnd  10705  bernneq  10769  faclbnd  10850  faclbnd3  10852  facavg  10855  crre  11039  remim  11042  mulreap  11046  amgm2  11300  fprodrecl  11790  fprodreclf  11796  efcllemp  11840  ege2le3  11853  ef01bndlem  11938  cos01gt0  11945  4sqlem11  12595  dveflem  15046  sinq12gt0  15150  tangtx  15158  coskpi  15168  relogexp  15192  logcxp  15217  rpabscxpbnd  15260