---

Step * of Lemma sum_difference

∀[n:ℕ]. ∀[f,g:ℕn ⟶ ℤ]. ∀[d:ℤ].  Σ(f[x] | x < n) = (Σ(g[x] | x < n) + d) ∈ ℤ supposing Σ(f[x] - g[x] | x < n) = d ∈ ℤ
BY
{ (Auto THEN RevHypSubstSq (-1) 0) }

1
1. n : ℕ
2. f : ℕn ⟶ ℤ
3. g : ℕn ⟶ ℤ
4. d : ℤ
5. Σ(f[x] - g[x] | x < n) = d ∈ ℤ
⊢ Σ(f[x] | x < n) = (Σ(g[x] | x < n) + Σ(f[x] - g[x] | x < n)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[d:\mBbbZ{}].
    \mSigma{}(f[x]  |  x  <  n)  =  (\mSigma{}(g[x]  |  x  <  n)  +  d)  supposing  \mSigma{}(f[x]  -  g[x]  |  x  <  n)  =  d


By

---

Latex:
(Auto  THEN  RevHypSubstSq  (-1)  0)

---

Home Index