Theorem remulcl 7101

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

Assertion

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

Proof of Theorem remulcl

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

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1433  (class class class)co 5532  ℝcr 6980   · cmul 6986

This theorem was proved from axioms:  ax-mulrcl 7075

This theorem is referenced by:  remulcli  7133  remulcld  7149  axmulgt0  7184  msqge0  7716  mulge0  7719  recexaplem2  7742  recexap  7743  ltmul12a  7938  lemul12b  7939  mulgt1  7941  ltdivmul  7954  cju  8038  addltmul  8267  zmulcl  8404  irrmul  8732  rpmulcl  8758  ge0mulcl  9005  iccdil  9020  reexpcl  9493  reexpclzap  9496  expge0  9512  expge1  9513  expubnd  9533  bernneq  9593  faclbnd  9668  faclbnd3  9670  facavg  9673  crre  9744  remim  9747  mulreap  9751  amgm2  10004