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