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

Theorem remulcli 8001
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 7969 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3mp2an 426 1 (𝐴 · 𝐵) ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 2160  (class class class)co 5896  cr 7840   · cmul 7846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 7940
This theorem is referenced by:  addltmul  9185  nn0lele2xi  9257  numltc  9439  ef01bndlem  11796  cos2bnd  11800  sin4lt0  11806  sincosq3sgn  14706  sincosq4sgn  14707  cosq23lt0  14711  coseq0q4123  14712  coseq00topi  14713  coseq0negpitopi  14714  sincos4thpi  14718  cosq34lt1  14728  cos02pilt1  14729  cos0pilt1  14730  taupi  15280
  Copyright terms: Public domain W3C validator