---

Step * 1 1 1 1 of Lemma rless-iff-rpositive


1. x : ℝ@i
2. y : ℝ@i
3. ∀b:ℕ+. ∃n:ℕ+. ∀m:ℕ+. ((n ≤ m) ⇒ (b ≤ ((y m) - x m)))
4. n : ℕ+
5. ∀m:ℕ+. ((n ≤ m) ⇒ (20 ≤ ((y m) - x m)))
6. 20 ≤ ((y (4 * n)) - x (4 * n))
⊢ 4 < (y - x) n
BY
{ (RepUR ``rsub radd rminus accelerate`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (RWO "reg-seq-list-add-as-l_sum" 0 THENA Auto)
   THEN Reduce 0
   THEN Mul ⌜4⌝ 0⋅
   THEN (RWO "div_rem_sum2" 0 THENA Auto)) }

1
1. x : ℝ@i
2. y : ℝ@i
3. ∀b:ℕ+. ∃n:ℕ+. ∀m:ℕ+. ((n ≤ m) ⇒ (b ≤ ((y m) - x m)))
4. n : ℕ+
5. ∀m:ℕ+. ((n ≤ m) ⇒ (20 ≤ ((y m) - x m)))
6. 20 ≤ ((y (4 * n)) - x (4 * n))
⊢ 4 * 4 < ((y (4 * n)) + (-(x (4 * n))) + 0) - (y (4 * n)) + (-(x (4 * n))) + 0 rem 4

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}@i
2.  y  :  \mBbbR{}@i
3.  \mforall{}b:\mBbbN{}\msupplus{}.  \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}m:\mBbbN{}\msupplus{}.  ((n  \mleq{}  m)  {}\mRightarrow{}  (b  \mleq{}  ((y  m)  -  x  m)))
4.  n  :  \mBbbN{}\msupplus{}
5.  \mforall{}m:\mBbbN{}\msupplus{}.  ((n  \mleq{}  m)  {}\mRightarrow{}  (20  \mleq{}  ((y  m)  -  x  m)))
6.  20  \mleq{}  ((y  (4  *  n))  -  x  (4  *  n))
\mvdash{}  4  <  (y  -  x)  n


By

---

Latex:
(RepUR  ``rsub  radd  rminus  accelerate``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (RWO  "reg-seq-list-add-as-l\_sum"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Mul  \mkleeneopen{}4\mkleeneclose{}  0\mcdot{}
  THEN  (RWO  "div\_rem\_sum2"  0  THENA  Auto))

---

Home Index