---

Step * of Lemma int-rdiv-rless-witness

No Annotations
∀k:ℕ+. (k ∈ (r1)/k < (r(4))/k)
BY
{ (Intro
   THEN RepUR ``rless int-to-real int-rdiv`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Reduce 0
   THEN (Assert ¬k < 0 BY
               Auto)
   THEN (Reduce 0 THENA Auto)
   THEN MemTypeCD
   THEN Auto
   THEN (RW IntNormC 0 THENA Auto)) }

1
1. k : ℕ+
2. ¬k < 0
⊢ 4 + ((2 * k) ÷ k) < (8 * k) ÷ k

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}\msupplus{}.  (k  \mmember{}  (r1)/k  <  (r(4))/k)


By

---

Latex:
(Intro
  THEN  RepUR  ``rless  int-to-real  int-rdiv``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Assert  \mneg{}k  <  0  BY
                          Auto)
  THEN  (Reduce  0  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  (RW  IntNormC  0  THENA  Auto))

---

Home Index