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

Theorem remulcli 7949
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 7917 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
41, 2, 3mp2an 426 1 (𝐴 · 𝐵) ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 2148  (class class class)co 5868  cr 7788   · cmul 7794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulrcl 7888
This theorem is referenced by:  addltmul  9131  nn0lele2xi  9203  numltc  9385  ef01bndlem  11735  cos2bnd  11739  sin4lt0  11745  sincosq3sgn  13882  sincosq4sgn  13883  cosq23lt0  13887  coseq0q4123  13888  coseq00topi  13889  coseq0negpitopi  13890  sincos4thpi  13894  cosq34lt1  13904  cos02pilt1  13905  cos0pilt1  13906  taupi  14441
  Copyright terms: Public domain W3C validator