Theorem remulcl 7902

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141  (class class class)co 5853  ℝcr 7773   · cmul 7779

This theorem was proved from axioms:  ax-mulrcl 7873

This theorem is referenced by:  remulcli  7934  remulcld  7950  axmulgt0  7991  msqge0  8535  mulge0  8538  recexaplem2  8570  recexap  8571  ltmul12a  8776  lemul12b  8777  mulgt1  8779  ltdivmul  8792  cju  8877  addltmul  9114  zmulcl  9265  irrmul  9606  rpmulcl  9635  ge0mulcl  9939  iccdil  9955  reexpcl  10493  reexpclzap  10496  expge0  10512  expge1  10513  expubnd  10533  bernneq  10596  faclbnd  10675  faclbnd3  10677  facavg  10680  crre  10821  remim  10824  mulreap  10828  amgm2  11082  fprodrecl  11571  fprodreclf  11577  efcllemp  11621  ege2le3  11634  ef01bndlem  11719  cos01gt0  11725  dveflem  13481  sinq12gt0  13545  tangtx  13553  coskpi  13563  relogexp  13587  logcxp  13612  rpabscxpbnd  13653