Theorem remulcl 8123

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6000  ℝcr 7994   · cmul 8000

This theorem was proved from axioms:  ax-mulrcl 8094

This theorem is referenced by:  remulcli  8156  remulcld  8173  axmulgt0  8214  msqge0  8759  mulge0  8762  recexaplem2  8795  recexap  8796  ltmul12a  9003  lemul12b  9004  mulgt1  9006  ltdivmul  9019  cju  9104  addltmul  9344  zmulcl  9496  irrmul  9838  rpmulcl  9870  ge0mulcl  10174  iccdil  10190  reexpcl  10773  reexpclzap  10776  expge0  10792  expge1  10793  expubnd  10813  bernneq  10877  faclbnd  10958  faclbnd3  10960  facavg  10963  crre  11363  remim  11366  mulreap  11370  amgm2  11624  fprodrecl  12114  fprodreclf  12120  efcllemp  12164  ege2le3  12177  ef01bndlem  12262  cos01gt0  12269  4sqlem11  12919  dveflem  15394  sinq12gt0  15498  tangtx  15506  coskpi  15516  relogexp  15540  logcxp  15565  rpabscxpbnd  15608