---

Step * of Lemma isolate_summand

∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[m:ℕn].  (Σ(f[x] | x < n) = (f[m] + Σ(if (x =z m) then 0 else f[x] fi  | x < n)) ∈ ℤ)
BY
{ (((D 0 THENA Auto) THEN NatInd 1) THEN Reduce 0 THEN ((ParallelOp (-1) THEN Auto) ORELSE Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[m:\mBbbN{}n].
    (\mSigma{}(f[x]  |  x  <  n)  =  (f[m]  +  \mSigma{}(if  (x  =\msubz{}  m)  then  0  else  f[x]  fi    |  x  <  n)))


By

---

Latex:
(((D  0  THENA  Auto)  THEN  NatInd  1)  THEN  Reduce  0  THEN  ((ParallelOp  (-1)  THEN  Auto)  ORELSE  Auto))

---

Home Index