---

Step * of Lemma sum_split+

∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[m:ℕn + 1].
  ((Σ(f[x] | x < n) = (Σ(f[x] | x < m) + Σ(f[x + m] | x < n - m)) ∈ ℤ)
  ∧ (Σ(f[x] | x < m) ∈ ℤ)
  ∧ (Σ(f[x + m] | x < n - m) ∈ ℤ))
BY
{ (InstLemma `sum_split` [] THEN RepeatFor 3 (ParallelLast') THEN D 0 THEN Try (Trivial) THEN Thin (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[m:\mBbbN{}n  +  1].
    ((\mSigma{}(f[x]  |  x  <  n)  =  (\mSigma{}(f[x]  |  x  <  m)  +  \mSigma{}(f[x  +  m]  |  x  <  n  -  m)))
    \mwedge{}  (\mSigma{}(f[x]  |  x  <  m)  \mmember{}  \mBbbZ{})
    \mwedge{}  (\mSigma{}(f[x  +  m]  |  x  <  n  -  m)  \mmember{}  \mBbbZ{}))


By

---

Latex:
(InstLemma  `sum\_split`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  D  0
  THEN  Try  (Trivial)
  THEN  Thin  (-1)\mcdot{}
  THEN  Auto)

---

Home Index