---

Step * 3 1 of Lemma regularize-k-regular


1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. m : ℕ+
4. ¬↑regular-upto(k;m;f)
5. n : ℕ+
6. ↑regular-upto(k;n;f)
7. v : ℕ
8. ¬↑regular-upto(k;v;f)
9. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
10. ¬(v = 1 ∈ ℤ)
11. ¬(v = 0 ∈ ℤ)
12. j : ℕ+
13. (v - 1) = j ∈ ℕ+
⊢ ∃z@0:ℝ
   ((((r(eval j = seq-min-upper(k;j;f) in
         k * ((m * ((f j) + (2 * k))) ÷ j * k) - 2 * k)/r((2 * k) * m)) ≤ z@0)
    ∧ (z@0 ≤ (r(eval j = seq-min-upper(k;j;f) in k * ((m * ((f j) + (2 * k))) ÷ j * k) + (2 * k))/r((2 * k) * m))))
   ∧ ((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z@0)
   ∧ (z@0 ≤ (r((f n) + (2 * k))/r((2 * k) * n))))
BY
{ ((Assert ↑regular-upto(k;j;f) BY
          ((Assert ¬¬↑regular-upto(k;j;f) BY
                  Auto)
           THEN MoveToConcl (-1)
           THEN BoolCase ⌜regular-upto(k;j;f)⌝⋅
           THEN Auto))
   THEN (RWO "regular-upto-iff" (-1) THENA Auto)
   ) }

1
1. k : ℕ+
2. f : ℕ+ ⟶ ℤ
3. m : ℕ+
4. ¬↑regular-upto(k;m;f)
5. n : ℕ+
6. ↑regular-upto(k;n;f)
7. v : ℕ
8. ¬↑regular-upto(k;v;f)
9. ∀[i:ℕ]. ¬¬↑regular-upto(k;i;f) supposing i < v
10. ¬(v = 1 ∈ ℤ)
11. ¬(v = 0 ∈ ℤ)
12. j : ℕ+
13. (v - 1) = j ∈ ℕ+
14. ∀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)))
⊢ ∃z@0:ℝ
   ((((r(eval j = seq-min-upper(k;j;f) in
         k * ((m * ((f j) + (2 * k))) ÷ j * k) - 2 * k)/r((2 * k) * m)) ≤ z@0)
    ∧ (z@0 ≤ (r(eval j = seq-min-upper(k;j;f) in k * ((m * ((f j) + (2 * k))) ÷ j * k) + (2 * k))/r((2 * k) * m))))
   ∧ ((r((f n) - 2 * k)/r((2 * k) * n)) ≤ z@0)
   ∧ (z@0 ≤ (r((f n) + (2 * k))/r((2 * k) * n))))

---

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  :  \mBbbN{}\msupplus{}
6.  \muparrow{}regular-upto(k;n;f)
7.  v  :  \mBbbN{}
8.  \mneg{}\muparrow{}regular-upto(k;v;f)
9.  \mforall{}[i:\mBbbN{}].  \mneg{}\mneg{}\muparrow{}regular-upto(k;i;f)  supposing  i  <  v
10.  \mneg{}(v  =  1)
11.  \mneg{}(v  =  0)
12.  j  :  \mBbbN{}\msupplus{}
13.  (v  -  1)  =  j
\mvdash{}  \mexists{}z@0:\mBbbR{}
      ((((r(eval  j  =  seq-min-upper(k;j;f)  in
                  k  *  ((m  *  ((f  j)  +  (2  *  k)))  \mdiv{}  j  *  k)  -  2  *  k)/r((2  *  k)  *  m))  \mleq{}  z@0)
        \mwedge{}  (z@0  \mleq{}  (r(eval  j  =  seq-min-upper(k;j;f)  in  k  *  ((m  *  ((f  j)  +  (2  *  k)))  \mdiv{}  j  *  k)  +  (2  *  k))/r(\000C(2  *  k)
            *  m))))
      \mwedge{}  ((r((f  n)  -  2  *  k)/r((2  *  k)  *  n))  \mleq{}  z@0)
      \mwedge{}  (z@0  \mleq{}  (r((f  n)  +  (2  *  k))/r((2  *  k)  *  n))))


By

---

Latex:
((Assert  \muparrow{}regular-upto(k;j;f)  BY
                ((Assert  \mneg{}\mneg{}\muparrow{}regular-upto(k;j;f)  BY
                                Auto)
                  THEN  MoveToConcl  (-1)
                  THEN  BoolCase  \mkleeneopen{}regular-upto(k;j;f)\mkleeneclose{}\mcdot{}
                  THEN  Auto))
  THEN  (RWO  "regular-upto-iff"  (-1)  THENA  Auto)
  )

---

Home Index