---

Step * of Lemma regular-upto-iff

∀k,b:ℕ+. ∀x:ℕ+ ⟶ ℤ.
  (↑regular-upto(k;b;x)
  ⇐⇒ ∀n,m:ℕ+b + 1.
        let j = seq-min-upper(k;b;x) in
         let z = (r((x j) + (2 * k))/r((2 * k) * j)) in
         (((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. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. ↑regular-upto(k;b;x)
5. n : ℕ+b + 1
6. m : ℕ+b + 1
⊢ let j = seq-min-upper(k;b;x) in
   let z = (r((x j) + (2 * k))/r((2 * k) * j)) in
   (((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. b : ℕ+
3. x : ℕ+ ⟶ ℤ
4. ∀n,m:ℕ+b + 1.
     let j = seq-min-upper(k;b;x) in
      let z = (r((x j) + (2 * k))/r((2 * k) * j)) in
      (((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)))
⊢ ↑regular-upto(k;b;x)

---

Latex:

---

Latex:
\mforall{}k,b:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.
    (\muparrow{}regular-upto(k;b;x)
    \mLeftarrow{}{}\mRightarrow{}  \mforall{}n,m:\mBbbN{}\msupplus{}b  +  1.
                let  j  =  seq-min-upper(k;b;x)  in
                  let  z  =  (r((x  j)  +  (2  *  k))/r((2  *  k)  *  j))  in
                  (((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