---

Step * of Lemma summand-le-sum

No Annotations
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  ∀[i:ℕn]. (f[i] ≤ Σ(f[x] | x < n)) supposing ∀x:ℕn. (0 ≤ f[x])
BY
{ (InstLemma `isolate_summand` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN ParallelOp -2
   THEN Thin 3
   THEN (HypSubst' (-1) 0 THENA Auto)) }

1
1. n : ℕ
2. f : ℕn ⟶ ℤ
3. ∀x:ℕn. (0 ≤ f[x])
4. [i] : ℕn
5. Σ(f[x] | x < n) = (f[i] + Σ(if (x =z i) then 0 else f[x] fi  | x < n)) ∈ ℤ
⊢ f[i] ≤ (f[i] + Σ(if (x =z i) then 0 else f[x] fi  | x < n))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].    \mforall{}[i:\mBbbN{}n].  (f[i]  \mleq{}  \mSigma{}(f[x]  |  x  <  n))  supposing  \mforall{}x:\mBbbN{}n.  (0  \mleq{}  f[x])


By

---

Latex:
(InstLemma  `isolate\_summand`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  Thin  3
  THEN  (HypSubst'  (-1)  0  THENA  Auto))

---

Home Index