Theorem remulcl 7941

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  (class class class)co 5877  ℝcr 7812   · cmul 7818

This theorem was proved from axioms:  ax-mulrcl 7912

This theorem is referenced by:  remulcli  7973  remulcld  7990  axmulgt0  8031  msqge0  8575  mulge0  8578  recexaplem2  8611  recexap  8612  ltmul12a  8819  lemul12b  8820  mulgt1  8822  ltdivmul  8835  cju  8920  addltmul  9157  zmulcl  9308  irrmul  9649  rpmulcl  9680  ge0mulcl  9984  iccdil  10000  reexpcl  10539  reexpclzap  10542  expge0  10558  expge1  10559  expubnd  10579  bernneq  10643  faclbnd  10723  faclbnd3  10725  facavg  10728  crre  10868  remim  10871  mulreap  10875  amgm2  11129  fprodrecl  11618  fprodreclf  11624  efcllemp  11668  ege2le3  11681  ef01bndlem  11766  cos01gt0  11772  dveflem  14226  sinq12gt0  14290  tangtx  14298  coskpi  14308  relogexp  14332  logcxp  14357  rpabscxpbnd  14398