---

Step * 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
⊢ ((i
  * (f 
     if (n * (f seq-min-upper(k;n - 1;f))) + ((2 * k) * n) ≤z (seq-min-upper(k;n - 1;f) * (f n))
        + ((2 * k) * seq-min-upper(k;n - 1;f))
     then seq-min-upper(k;n - 1;f)
     else n
     fi )) - if (n * (f seq-min-upper(k;n - 1;f))) + ((2 * k) * n) ≤z (seq-min-upper(k;n - 1;f) * (f n))
                + ((2 * k) * seq-min-upper(k;n - 1;f))
  then seq-min-upper(k;n - 1;f)
  else n
  fi 
  * (f i)) ≤ ((2 * k)
  * (if (n * (f seq-min-upper(k;n - 1;f))) + ((2 * k) * n) ≤z (seq-min-upper(k;n - 1;f) * (f n))
        + ((2 * k) * seq-min-upper(k;n - 1;f))
    then seq-min-upper(k;n - 1;f)
    else n
    fi  - i))
BY
{ ((Decide ⌜i = n ∈ ℤ⌝⋅ THENA Auto)
   THENL [(HypSubst' (-1) 0 THEN AutoSplit THEN Auto); ((InstHyp [⌜i⌝] (-3)⋅ THENA Auto) THEN AutoSplit)]
) }

1
1. k : ℕ
2. f : ℕ+ ⟶ ℤ
3. n : ℤ
4. ¬(((n * (f seq-min-upper(k;n - 1;f))) + ((2 * k) * n)) ≤ ((seq-min-upper(k;n - 1;f) * (f n))
     + ((2 * k) * seq-min-upper(k;n - 1;f))))
5. 0 < n
6. ∀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)))
7. i : ℕ+n + 1
8. ¬(i = n ∈ ℤ)
9. ((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))
⊢ ((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
\mvdash{}  ((i
    *  (f 
          if  (n  *  (f  seq-min-upper(k;n  -  1;f)))  +  ((2  *  k)  *  n)  \mleq{}z  (seq-min-upper(k;n  -  1;f)  *  (f  n))
                +  ((2  *  k)  *  seq-min-upper(k;n  -  1;f))
          then  seq-min-upper(k;n  -  1;f)
          else  n
          fi  ))  -  if  (n  *  (f  seq-min-upper(k;n  -  1;f)))  +  ((2  *  k)  *  n)  \mleq{}z  (seq-min-upper(k;n  -  1;f)
                                *  (f  n))
                                +  ((2  *  k)  *  seq-min-upper(k;n  -  1;f))
    then  seq-min-upper(k;n  -  1;f)
    else  n
    fi 
    *  (f  i))  \mleq{}  ((2  *  k)
    *  (if  (n  *  (f  seq-min-upper(k;n  -  1;f)))  +  ((2  *  k)  *  n)  \mleq{}z  (seq-min-upper(k;n  -  1;f)  *  (f  n))
                +  ((2  *  k)  *  seq-min-upper(k;n  -  1;f))
        then  seq-min-upper(k;n  -  1;f)
        else  n
        fi    -  i))


By

---

Latex:
((Decide  \mkleeneopen{}i  =  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENL  [(HypSubst'  (-1)  0  THEN  AutoSplit  THEN  Auto)
              ;  ((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  AutoSplit)]
)

---

Home Index