Theorem remulcl 7854

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2128  (class class class)co 5821  ℝcr 7725   · cmul 7731

This theorem was proved from axioms:  ax-mulrcl 7825

This theorem is referenced by:  remulcli  7886  remulcld  7902  axmulgt0  7943  msqge0  8485  mulge0  8488  recexaplem2  8520  recexap  8521  ltmul12a  8725  lemul12b  8726  mulgt1  8728  ltdivmul  8741  cju  8826  addltmul  9063  zmulcl  9214  irrmul  9549  rpmulcl  9578  ge0mulcl  9879  iccdil  9895  reexpcl  10429  reexpclzap  10432  expge0  10448  expge1  10449  expubnd  10469  bernneq  10531  faclbnd  10608  faclbnd3  10610  facavg  10613  crre  10750  remim  10753  mulreap  10757  amgm2  11011  fprodrecl  11498  fprodreclf  11504  efcllemp  11548  ege2le3  11561  ef01bndlem  11646  cos01gt0  11652  dveflem  13058  sinq12gt0  13122  tangtx  13130  coskpi  13140  relogexp  13164  logcxp  13189  rpabscxpbnd  13230