---

Step * of Lemma pair_support

∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[m,k:ℕn].
  (Σ(f[x] | x < n) = (f[m] + f[k]) ∈ ℤ) supposing 
     ((∀x:ℕn. ((¬(x = m ∈ ℤ)) ⇒ (¬(x = k ∈ ℤ)) ⇒ (f[x] = 0 ∈ ℤ))) and 
     (¬(m = k ∈ ℤ)))
BY
{ Auto }

1
1. n : ℕ
2. f : ℕn ⟶ ℤ
3. m : ℕn
4. k : ℕn
5. ¬(m = k ∈ ℤ)
6. ∀x:ℕn. ((¬(x = m ∈ ℤ)) ⇒ (¬(x = k ∈ ℤ)) ⇒ (f[x] = 0 ∈ ℤ))
⊢ Σ(f[x] | x < n) = (f[m] + f[k]) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[m,k:\mBbbN{}n].
    (\mSigma{}(f[x]  |  x  <  n)  =  (f[m]  +  f[k]))  supposing 
          ((\mforall{}x:\mBbbN{}n.  ((\mneg{}(x  =  m))  {}\mRightarrow{}  (\mneg{}(x  =  k))  {}\mRightarrow{}  (f[x]  =  0)))  and 
          (\mneg{}(m  =  k)))


By

---

Latex:
Auto

---

Home Index