---

Step * of Lemma regular-less

∀[x,y:ℝ].  ∀n:ℕ+. ((x n) + 4 < y n ⇒ (∀m:ℕ+. ((x m) ≤ ((y m) + 4))))
BY
{ (Auto
   THEN Mul ⌜m⌝ (-2)⋅
   THEN Mul ⌜n⌝ 0⋅
   THEN Assert ⌜((m * (y n)) - 2 * (n + m)) ≤ (n * (y m))⌝ ∧ ((n * (x m)) ≤ ((m * (x n)) + (2 * (n + m))))⋅
   THEN Auto'
   THEN All Thin
   THEN D 1
   THEN Unhide
   THEN Auto
   THEN Unfold `regular-int-seq` 2
   THEN (InstHyp [⌜n⌝;⌜m⌝] 2⋅ THENA Auto)
   THEN (RWO  "absval_ifthenelse" (-1) THENA Auto)
   THEN SplitOnHypITE -1 
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    \mforall{}n:\mBbbN{}\msupplus{}.  ((x  n)  +  4  <  y  n  {}\mRightarrow{}  (\mforall{}m:\mBbbN{}\msupplus{}.  ((x  m)  \mleq{}  ((y  m)  +  4))))


By

---

Latex:
(Auto
  THEN  Mul  \mkleeneopen{}m\mkleeneclose{}  (-2)\mcdot{}
  THEN  Mul  \mkleeneopen{}n\mkleeneclose{}  0\mcdot{}
  THEN  Assert  \mkleeneopen{}((m  *  (y  n))  -  2  *  (n  +  m))  \mleq{}  (n  *  (y  m))\mkleeneclose{}
  \mwedge{}  ((n  *  (x  m))  \mleq{}  ((m  *  (x  n))  +  (2  *  (n  +  m))))\mcdot{}
  THEN  Auto'
  THEN  All  Thin
  THEN  D  1
  THEN  Unhide
  THEN  Auto
  THEN  Unfold  `regular-int-seq`  2
  THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
  THEN  (RWO    "absval\_ifthenelse"  (-1)  THENA  Auto)
  THEN  SplitOnHypITE  -1 
  THEN  Auto')

---

Home Index