Theorem remulcl 8307

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

Assertion

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

Proof of Theorem remulcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  (class class class)co 6085  ℝcr 8178   · cmul 8184

This proof depends on axioms:  ax-mulrcl 8278

This theorem is used by:  remulcli  8340  remulcld  8356  axmulgt0  8397  msqge0  8946  mulge0  8949  recexaplem2  8982  recexap  8983  ltmul12a  9192  lemul12b  9193  mulgt1  9195  ltdivmul  9208  cju  9293  addltmul  9546  zmulcl  9702  irrmul  10057  rpmulcl  10089  ge0mulcl  10394  iccdil  10410  reexpcl  11006  reexpclzap  11009  expge0  11025  expge1  11026  expubnd  11046  bernneq  11111  faclbnd  11193  faclbnd3  11195  facavg  11198  crre  11636  remim  11639  mulreap  11643  amgm2  11899  fprodrecl  12391  fprodreclf  12397  efcllemp  12441  ege2le3  12454  ef01bndlem  12539  cos01gt0  12546  4sqlem11  13200  dveflem  15876  sinq12gt0  15981  tangtx  15989  coskpi  15999  relogexp  16024  logfac  16048  logcxp  16052  rpabscxpbnd  16095  bpos1lem  16207  bposlem1  16209  bposlem2  16210