---

Step * of Lemma regular-iff

∀x:ℕ+ ⟶ ℤ
  (regular-seq(x)
  ⇐⇒ ∀n,m:ℕ+.
        ∃z:ℝ
         ((((r((x n) - 2)/r(2 * n)) ≤ z) ∧ (z ≤ (r((x n) + 2)/r(2 * n))))
         ∧ ((r((x m) - 2)/r(2 * m)) ≤ z)
         ∧ (z ≤ (r((x m) + 2)/r(2 * m)))))
BY
{ ((InstLemma `regular-int-seq-iff` [⌜1⌝]⋅ THENA Auto) THEN ParallelLast' THEN Subst' 2 * 1 ~ 2 -1 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
    (regular-seq(x)
    \mLeftarrow{}{}\mRightarrow{}  \mforall{}n,m:\mBbbN{}\msupplus{}.
                \mexists{}z:\mBbbR{}
                  ((((r((x  n)  -  2)/r(2  *  n))  \mleq{}  z)  \mwedge{}  (z  \mleq{}  (r((x  n)  +  2)/r(2  *  n))))
                  \mwedge{}  ((r((x  m)  -  2)/r(2  *  m))  \mleq{}  z)
                  \mwedge{}  (z  \mleq{}  (r((x  m)  +  2)/r(2  *  m)))))


By

---

Latex:
((InstLemma  `regular-int-seq-iff`  [\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast'
  THEN  Subst'  2  *  1  \msim{}  2  -1
  THEN  Auto)

---

Home Index