Theorem remulcl 8271

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  (class class class)co 6058  ℝcr 8142   · cmul 8148

This theorem was proved from axioms:  ax-mulrcl 8242

This theorem is referenced by:  remulcli  8304  remulcld  8320  axmulgt0  8361  msqge0  8907  mulge0  8910  recexaplem2  8943  recexap  8944  ltmul12a  9151  lemul12b  9152  mulgt1  9154  ltdivmul  9167  cju  9252  addltmul  9492  zmulcl  9648  irrmul  9997  rpmulcl  10029  ge0mulcl  10334  iccdil  10350  reexpcl  10942  reexpclzap  10945  expge0  10961  expge1  10962  expubnd  10982  bernneq  11047  faclbnd  11128  faclbnd3  11130  facavg  11133  crre  11567  remim  11570  mulreap  11574  amgm2  11828  fprodrecl  12319  fprodreclf  12325  efcllemp  12369  ege2le3  12382  ef01bndlem  12467  cos01gt0  12474  4sqlem11  13124  dveflem  15717  sinq12gt0  15821  tangtx  15829  coskpi  15839  relogexp  15863  logcxp  15888  rpabscxpbnd  15931