Theorem remulcl 8026

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

Assertion

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

Proof of Theorem remulcl

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

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

This theorem was proved from axioms:  ax-mulrcl 7997

This theorem is referenced by:  remulcli  8059  remulcld  8076  axmulgt0  8117  msqge0  8662  mulge0  8665  recexaplem2  8698  recexap  8699  ltmul12a  8906  lemul12b  8907  mulgt1  8909  ltdivmul  8922  cju  9007  addltmul  9247  zmulcl  9398  irrmul  9740  rpmulcl  9772  ge0mulcl  10076  iccdil  10092  reexpcl  10667  reexpclzap  10670  expge0  10686  expge1  10687  expubnd  10707  bernneq  10771  faclbnd  10852  faclbnd3  10854  facavg  10857  crre  11041  remim  11044  mulreap  11048  amgm2  11302  fprodrecl  11792  fprodreclf  11798  efcllemp  11842  ege2le3  11855  ef01bndlem  11940  cos01gt0  11947  4sqlem11  12597  dveflem  15070  sinq12gt0  15174  tangtx  15182  coskpi  15192  relogexp  15216  logcxp  15241  rpabscxpbnd  15284