---

Step * of Lemma seq-max-lower-le

∀[k:ℕ]. ∀[n:ℕ+]. ∀[f:ℕ+ ⟶ ℤ].  (seq-max-lower(k;n;f) ≤ n)
BY
{ (Auto THEN (NatPlusInd 2⋅ THENA Auto) THEN Unfold `seq-max-lower` 0 THEN Reduce 0 THEN Auto) }

1
1. k : ℕ
2. f : ℕ+ ⟶ ℤ
3. n : ℤ
4. 0 < n
5. seq-max-lower(k;n;f) ≤ n
⊢ primrec(n + 1;1;λi,r. if ((i + 1) * (f r)) - (2 * k) * (i + 1) ≤z (r * (f (i + 1))) - (2 * k) * r
                       then i + 1
                       else r
                       fi ) ≤ (n + 1)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].    (seq-max-lower(k;n;f)  \mleq{}  n)


By

---

Latex:
(Auto  THEN  (NatPlusInd  2\mcdot{}  THENA  Auto)  THEN  Unfold  `seq-max-lower`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index