Theorem remulcl 8073

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  (class class class)co 5957  ℝcr 7944   · cmul 7950

This theorem was proved from axioms:  ax-mulrcl 8044

This theorem is referenced by:  remulcli  8106  remulcld  8123  axmulgt0  8164  msqge0  8709  mulge0  8712  recexaplem2  8745  recexap  8746  ltmul12a  8953  lemul12b  8954  mulgt1  8956  ltdivmul  8969  cju  9054  addltmul  9294  zmulcl  9446  irrmul  9788  rpmulcl  9820  ge0mulcl  10124  iccdil  10140  reexpcl  10723  reexpclzap  10726  expge0  10742  expge1  10743  expubnd  10763  bernneq  10827  faclbnd  10908  faclbnd3  10910  facavg  10913  crre  11243  remim  11246  mulreap  11250  amgm2  11504  fprodrecl  11994  fprodreclf  12000  efcllemp  12044  ege2le3  12057  ef01bndlem  12142  cos01gt0  12149  4sqlem11  12799  dveflem  15273  sinq12gt0  15377  tangtx  15385  coskpi  15395  relogexp  15419  logcxp  15444  rpabscxpbnd  15487