---

Step * of Lemma regular-int-seq-iff

∀k:ℕ+. ∀x:ℕ+ ⟶ ℤ.
  (k-regular-seq(x)
  ⇐⇒ ∀n,m:ℕ+.
        ∃z:ℝ
         ((((r((x n) - 2 * k)/r((2 * k) * n)) ≤ z) ∧ (z ≤ (r((x n) + (2 * k))/r((2 * k) * n))))
         ∧ ((r((x m) - 2 * k)/r((2 * k) * m)) ≤ z)
         ∧ (z ≤ (r((x m) + (2 * k))/r((2 * k) * m)))))
BY
{ Auto }

1
1. k : ℕ+
2. x : ℕ+ ⟶ ℤ
3. k-regular-seq(x)
4. n : ℕ+
5. m : ℕ+
⊢ ∃z:ℝ
   ((((r((x n) - 2 * k)/r((2 * k) * n)) ≤ z) ∧ (z ≤ (r((x n) + (2 * k))/r((2 * k) * n))))
   ∧ ((r((x m) - 2 * k)/r((2 * k) * m)) ≤ z)
   ∧ (z ≤ (r((x m) + (2 * k))/r((2 * k) * m))))

2
1. k : ℕ+
2. x : ℕ+ ⟶ ℤ
3. ∀n,m:ℕ+.
     ∃z:ℝ
      ((((r((x n) - 2 * k)/r((2 * k) * n)) ≤ z) ∧ (z ≤ (r((x n) + (2 * k))/r((2 * k) * n))))
      ∧ ((r((x m) - 2 * k)/r((2 * k) * m)) ≤ z)
      ∧ (z ≤ (r((x m) + (2 * k))/r((2 * k) * m))))
⊢ k-regular-seq(x)

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index