---

Step * 1 1 1 1 of Lemma seq-min-upper-property


1. k : ℕ
2. f : ℕ+ ⟶ ℤ
3. n : ℤ
4. 0 < n
5. ∀i:ℕ+n
     (((i * (f seq-min-upper(k;n - 1;f))) - seq-min-upper(k;n - 1;f) * (f i)) ≤ ((2 * k)
      * (seq-min-upper(k;n - 1;f) - i)))
6. i : ℕ+n + 1
7. ¬(i = n ∈ ℤ)
8. v : ℕ+
9. seq-min-upper(k;n - 1;f) = v ∈ ℕ+
10. ¬(((n * (f v)) + ((2 * k) * n)) ≤ ((v * (f n)) + ((2 * k) * v)))
⊢ (((i * (f v)) - v * (f i)) ≤ ((2 * k) * (v - i))) ⇒ (((i * (f n)) - n * (f i)) ≤ ((2 * k) * (n - i)))
BY
{ ((Assert (v * (f n)) + ((2 * k) * v) < (n * (f v)) + ((2 * k) * n) BY Auto) THEN Auto) }

1
1. k : ℕ
2. f : ℕ+ ⟶ ℤ
3. n : ℤ
4. 0 < n
5. ∀i:ℕ+n
     (((i * (f seq-min-upper(k;n - 1;f))) - seq-min-upper(k;n - 1;f) * (f i)) ≤ ((2 * k)
      * (seq-min-upper(k;n - 1;f) - i)))
6. i : ℕ+n + 1
7. ¬(i = n ∈ ℤ)
8. v : ℕ+
9. seq-min-upper(k;n - 1;f) = v ∈ ℕ+
10. ¬(((n * (f v)) + ((2 * k) * n)) ≤ ((v * (f n)) + ((2 * k) * v)))
11. (v * (f n)) + ((2 * k) * v) < (n * (f v)) + ((2 * k) * n)
12. ((i * (f v)) - v * (f i)) ≤ ((2 * k) * (v - i))
⊢ ((i * (f n)) - n * (f i)) ≤ ((2 * k) * (n - i))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  \mforall{}i:\mBbbN{}\msupplus{}n
          (((i  *  (f  seq-min-upper(k;n  -  1;f)))  -  seq-min-upper(k;n  -  1;f)  *  (f  i))  \mleq{}  ((2  *  k)
            *  (seq-min-upper(k;n  -  1;f)  -  i)))
6.  i  :  \mBbbN{}\msupplus{}n  +  1
7.  \mneg{}(i  =  n)
8.  v  :  \mBbbN{}\msupplus{}
9.  seq-min-upper(k;n  -  1;f)  =  v
10.  \mneg{}(((n  *  (f  v))  +  ((2  *  k)  *  n))  \mleq{}  ((v  *  (f  n))  +  ((2  *  k)  *  v)))
\mvdash{}  (((i  *  (f  v))  -  v  *  (f  i))  \mleq{}  ((2  *  k)  *  (v  -  i)))
{}\mRightarrow{}  (((i  *  (f  n))  -  n  *  (f  i))  \mleq{}  ((2  *  k)  *  (n  -  i)))


By

---

Latex:
((Assert  (v  *  (f  n))  +  ((2  *  k)  *  v)  <  (n  *  (f  v))  +  ((2  *  k)  *  n)  BY  Auto)  THEN  Auto)

---

Home Index