Theorem remulcl 8203

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  (class class class)co 6028  ℝcr 8074   · cmul 8080

This theorem was proved from axioms:  ax-mulrcl 8174

This theorem is referenced by:  remulcli  8236  remulcld  8252  axmulgt0  8293  msqge0  8838  mulge0  8841  recexaplem2  8874  recexap  8875  ltmul12a  9082  lemul12b  9083  mulgt1  9085  ltdivmul  9098  cju  9183  addltmul  9423  zmulcl  9577  irrmul  9925  rpmulcl  9957  ge0mulcl  10261  iccdil  10277  reexpcl  10864  reexpclzap  10867  expge0  10883  expge1  10884  expubnd  10904  bernneq  10968  faclbnd  11049  faclbnd3  11051  facavg  11054  crre  11480  remim  11483  mulreap  11487  amgm2  11741  fprodrecl  12232  fprodreclf  12238  efcllemp  12282  ege2le3  12295  ef01bndlem  12380  cos01gt0  12387  4sqlem11  13037  dveflem  15520  sinq12gt0  15624  tangtx  15632  coskpi  15642  relogexp  15666  logcxp  15691  rpabscxpbnd  15734