Theorem remulcl 8138

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6007  ℝcr 8009   · cmul 8015

This theorem was proved from axioms:  ax-mulrcl 8109

This theorem is referenced by:  remulcli  8171  remulcld  8188  axmulgt0  8229  msqge0  8774  mulge0  8777  recexaplem2  8810  recexap  8811  ltmul12a  9018  lemul12b  9019  mulgt1  9021  ltdivmul  9034  cju  9119  addltmul  9359  zmulcl  9511  irrmul  9854  rpmulcl  9886  ge0mulcl  10190  iccdil  10206  reexpcl  10790  reexpclzap  10793  expge0  10809  expge1  10810  expubnd  10830  bernneq  10894  faclbnd  10975  faclbnd3  10977  facavg  10980  crre  11383  remim  11386  mulreap  11390  amgm2  11644  fprodrecl  12134  fprodreclf  12140  efcllemp  12184  ege2le3  12197  ef01bndlem  12282  cos01gt0  12289  4sqlem11  12939  dveflem  15415  sinq12gt0  15519  tangtx  15527  coskpi  15537  relogexp  15561  logcxp  15586  rpabscxpbnd  15629