---

Step * of Lemma rleq-implies

∀[x,y:ℝ].  ∀n:ℕ+. ((x (4 * n)) ≤ ((y (4 * n)) + 11)) supposing x ≤ y
BY
{ (Auto
   THEN RepUR ``rleq rnonneg rsub rminus radd accelerate`` -2
   THEN (With ⌜n⌝ (D (-2))⋅ THENA Auto)
   THEN (CallByValueReduce (-1) THENA Auto)
   THEN (RWO "reg-seq-list-add-as-l_sum" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN Mul ⌜4⌝ (-1)⋅
   THEN (RWO "div_rem_sum2" (-1) THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+@i
4. (-2) ≤ (((y (4 * n)) + (-(x (4 * n))) + 0) ÷ 4)
5. (4 * (-2)) ≤ (((y (4 * n)) + (-(x (4 * n))) + 0) - (y (4 * n)) + (-(x (4 * n))) + 0 rem 4)
⊢ (x (4 * n)) ≤ ((y (4 * n)) + 11)

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    \mforall{}n:\mBbbN{}\msupplus{}.  ((x  (4  *  n))  \mleq{}  ((y  (4  *  n))  +  11))  supposing  x  \mleq{}  y


By

---

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

---

Home Index