Theorem remulcl 8159

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  (class class class)co 6017  ℝcr 8030   · cmul 8036

This theorem was proved from axioms:  ax-mulrcl 8130

This theorem is referenced by:  remulcli  8192  remulcld  8209  axmulgt0  8250  msqge0  8795  mulge0  8798  recexaplem2  8831  recexap  8832  ltmul12a  9039  lemul12b  9040  mulgt1  9042  ltdivmul  9055  cju  9140  addltmul  9380  zmulcl  9532  irrmul  9880  rpmulcl  9912  ge0mulcl  10216  iccdil  10232  reexpcl  10817  reexpclzap  10820  expge0  10836  expge1  10837  expubnd  10857  bernneq  10921  faclbnd  11002  faclbnd3  11004  facavg  11007  crre  11417  remim  11420  mulreap  11424  amgm2  11678  fprodrecl  12168  fprodreclf  12174  efcllemp  12218  ege2le3  12231  ef01bndlem  12316  cos01gt0  12323  4sqlem11  12973  dveflem  15449  sinq12gt0  15553  tangtx  15561  coskpi  15571  relogexp  15595  logcxp  15620  rpabscxpbnd  15663