Theorem remulcl 8150

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6013  ℝcr 8021   · cmul 8027

This theorem was proved from axioms:  ax-mulrcl 8121

This theorem is referenced by:  remulcli  8183  remulcld  8200  axmulgt0  8241  msqge0  8786  mulge0  8789  recexaplem2  8822  recexap  8823  ltmul12a  9030  lemul12b  9031  mulgt1  9033  ltdivmul  9046  cju  9131  addltmul  9371  zmulcl  9523  irrmul  9871  rpmulcl  9903  ge0mulcl  10207  iccdil  10223  reexpcl  10808  reexpclzap  10811  expge0  10827  expge1  10828  expubnd  10848  bernneq  10912  faclbnd  10993  faclbnd3  10995  facavg  10998  crre  11408  remim  11411  mulreap  11415  amgm2  11669  fprodrecl  12159  fprodreclf  12165  efcllemp  12209  ege2le3  12222  ef01bndlem  12307  cos01gt0  12314  4sqlem11  12964  dveflem  15440  sinq12gt0  15544  tangtx  15552  coskpi  15562  relogexp  15586  logcxp  15611  rpabscxpbnd  15654