ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  remulcl GIF version

Theorem remulcl 7449
Description: Alias for ax-mulrcl 7423, for naming consistency with remulcli 7481. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
remulcl ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)

Proof of Theorem remulcl
StepHypRef Expression
1 ax-mulrcl 7423 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1438  (class class class)co 5634  cr 7328   · cmul 7334
This theorem was proved from axioms:  ax-mulrcl 7423
This theorem is referenced by:  remulcli  7481  remulcld  7497  axmulgt0  7537  msqge0  8069  mulge0  8072  recexaplem2  8095  recexap  8096  ltmul12a  8293  lemul12b  8294  mulgt1  8296  ltdivmul  8309  cju  8393  addltmul  8622  zmulcl  8773  irrmul  9101  rpmulcl  9127  ge0mulcl  9369  iccdil  9384  reexpcl  9937  reexpclzap  9940  expge0  9956  expge1  9957  expubnd  9977  bernneq  10039  faclbnd  10114  faclbnd3  10116  facavg  10119  crre  10256  remim  10259  mulreap  10263  amgm2  10516
  Copyright terms: Public domain W3C validator