Theorem remulcl 8255

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  (class class class)co 6050  ℝcr 8126   · cmul 8132

This theorem was proved from axioms:  ax-mulrcl 8226

This theorem is referenced by:  remulcli  8288  remulcld  8304  axmulgt0  8345  msqge0  8890  mulge0  8893  recexaplem2  8926  recexap  8927  ltmul12a  9134  lemul12b  9135  mulgt1  9137  ltdivmul  9150  cju  9235  addltmul  9475  zmulcl  9631  irrmul  9979  rpmulcl  10011  ge0mulcl  10315  iccdil  10331  reexpcl  10918  reexpclzap  10921  expge0  10937  expge1  10938  expubnd  10958  bernneq  11022  faclbnd  11103  faclbnd3  11105  facavg  11108  crre  11542  remim  11545  mulreap  11549  amgm2  11803  fprodrecl  12294  fprodreclf  12300  efcllemp  12344  ege2le3  12357  ef01bndlem  12442  cos01gt0  12449  4sqlem11  13099  dveflem  15591  sinq12gt0  15695  tangtx  15703  coskpi  15713  relogexp  15737  logcxp  15762  rpabscxpbnd  15805