---

Step * 3 1 1 1 of Lemma regularize-k-regular


1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. m : ℕ+
4. ¬↑regular-upto(k;m;f)
5. n : ℤ
6. 0 < n
7. ↑regular-upto(k;n;f)
8. v : ℕ
9. ¬↑regular-upto(k;v;f)
10. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
11. ¬(v = 1 ∈ ℤ)
12. ¬(v = 0 ∈ ℤ)
13. j : ℕ+
14. (v - 1) = j ∈ ℕ+
15. ∀n,m:ℕ+j + 1.
      let j = seq-min-upper(k;j;f) in
       let z = (r((f j) + (2 * k))/r((2 * k) * j)) in
       (((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z) ∧ (z ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
       ∧ ((r((f m) - 2 * k)/r((2 * k) * m)) ≤ z)
       ∧ (z ≤ (r((f m) + (2 * k))/r((2 * k) * m)))
⊢ n < j + 1
BY
{ (SupposeNot THEN (Assert ↑regular-upto(k;n;f) BY Hypothesis) THEN (Assert ⌜↑regular-upto(k;v;f)⌝⋅ THENM Auto)) }

1
.....assertion..... 
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. m : ℕ+
4. ¬↑regular-upto(k;m;f)
5. n : ℤ
6. 0 < n
7. ↑regular-upto(k;n;f)
8. v : ℕ
9. ¬↑regular-upto(k;v;f)
10. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
11. ¬(v = 1 ∈ ℤ)
12. ¬(v = 0 ∈ ℤ)
13. j : ℕ+
14. (v - 1) = j ∈ ℕ+
15. ∀n,m:ℕ+j + 1.
      let j = seq-min-upper(k;j;f) in
       let z = (r((f j) + (2 * k))/r((2 * k) * j)) in
       (((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z) ∧ (z ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
       ∧ ((r((f m) - 2 * k)/r((2 * k) * m)) ≤ z)
       ∧ (z ≤ (r((f m) + (2 * k))/r((2 * k) * m)))
16. ¬n < j + 1
17. ↑regular-upto(k;n;f)
⊢ ↑regular-upto(k;v;f)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  m  :  \mBbbN{}\msupplus{}
4.  \mneg{}\muparrow{}regular-upto(k;m;f)
5.  n  :  \mBbbZ{}
6.  0  <  n
7.  \muparrow{}regular-upto(k;n;f)
8.  v  :  \mBbbN{}
9.  \mneg{}\muparrow{}regular-upto(k;v;f)
10.  \mforall{}[i:\mBbbN{}].  \mneg{}\mneg{}\muparrow{}regular-upto(k;i;f)  supposing  i  <  v
11.  \mneg{}(v  =  1)
12.  \mneg{}(v  =  0)
13.  j  :  \mBbbN{}\msupplus{}
14.  (v  -  1)  =  j
15.  \mforall{}n,m:\mBbbN{}\msupplus{}j  +  1.
            let  j  =  seq-min-upper(k;j;f)  in
              let  z  =  (r((f  j)  +  (2  *  k))/r((2  *  k)  *  j))  in
              (((r((f  n)  -  2  *  k)/r((2  *  k)  *  n))  \mleq{}  z)  \mwedge{}  (z  \mleq{}  (r((f  n)  +  (2  *  k))/r((2  *  k)  *  n))))
              \mwedge{}  ((r((f  m)  -  2  *  k)/r((2  *  k)  *  m))  \mleq{}  z)
              \mwedge{}  (z  \mleq{}  (r((f  m)  +  (2  *  k))/r((2  *  k)  *  m)))
\mvdash{}  n  <  j  +  1


By

---

Latex:
(SupposeNot
  THEN  (Assert  \muparrow{}regular-upto(k;n;f)  BY
                          Hypothesis)
  THEN  (Assert  \mkleeneopen{}\muparrow{}regular-upto(k;v;f)\mkleeneclose{}\mcdot{}  THENM  Auto))

---

Home Index