Theorem remulcl 7741

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480  (class class class)co 5767  ℝcr 7612   · cmul 7618

This theorem was proved from axioms:  ax-mulrcl 7712

This theorem is referenced by:  remulcli  7773  remulcld  7789  axmulgt0  7829  msqge0  8371  mulge0  8374  recexaplem2  8406  recexap  8407  ltmul12a  8611  lemul12b  8612  mulgt1  8614  ltdivmul  8627  cju  8712  addltmul  8949  zmulcl  9100  irrmul  9432  rpmulcl  9459  ge0mulcl  9758  iccdil  9774  reexpcl  10303  reexpclzap  10306  expge0  10322  expge1  10323  expubnd  10343  bernneq  10405  faclbnd  10480  faclbnd3  10482  facavg  10485  crre  10622  remim  10625  mulreap  10629  amgm2  10883  efcllemp  11353  ege2le3  11366  ef01bndlem  11452  cos01gt0  11458  dveflem  12844  sinq12gt0  12900  tangtx  12908  coskpi  12918