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

Theorem remulcli 7792
Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
Hypotheses
Ref Expression
recni.1 𝐴 ∈ ℝ
axri.2 𝐵 ∈ ℝ
Assertion
Ref Expression
remulcli (𝐴 · 𝐵) ∈ ℝ

Proof of Theorem remulcli
StepHypRef Expression
1 recni.1 . 2 𝐴 ∈ ℝ
2 axri.2 . 2 𝐵 ∈ ℝ
3 remulcl 7760 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3mp2an 422 1 (𝐴 · 𝐵) ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1480  (class class class)co 5774  cr 7631   · cmul 7637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-mulrcl 7731
This theorem is referenced by:  addltmul  8968  nn0lele2xi  9040  numltc  9219  ef01bndlem  11474  cos2bnd  11478  sin4lt0  11484  sincosq3sgn  12931  sincosq4sgn  12932  cosq23lt0  12936  coseq0q4123  12937  coseq00topi  12938  coseq0negpitopi  12939  sincos4thpi  12943  cosq34lt1  12953  cos02pilt1  12954  cos0pilt1  12955  taupi  13330
  Copyright terms: Public domain W3C validator