Theorem remulcl 8160

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  (class class class)co 6018  ℝcr 8031   · cmul 8037

This theorem was proved from axioms:  ax-mulrcl 8131

This theorem is referenced by:  remulcli  8193  remulcld  8210  axmulgt0  8251  msqge0  8796  mulge0  8799  recexaplem2  8832  recexap  8833  ltmul12a  9040  lemul12b  9041  mulgt1  9043  ltdivmul  9056  cju  9141  addltmul  9381  zmulcl  9533  irrmul  9881  rpmulcl  9913  ge0mulcl  10217  iccdil  10233  reexpcl  10819  reexpclzap  10822  expge0  10838  expge1  10839  expubnd  10859  bernneq  10923  faclbnd  11004  faclbnd3  11006  facavg  11009  crre  11435  remim  11438  mulreap  11442  amgm2  11696  fprodrecl  12187  fprodreclf  12193  efcllemp  12237  ege2le3  12250  ef01bndlem  12335  cos01gt0  12342  4sqlem11  12992  dveflem  15469  sinq12gt0  15573  tangtx  15581  coskpi  15591  relogexp  15615  logcxp  15640  rpabscxpbnd  15683