Step
*
1
of Lemma
pair_support
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]) ∈ ℤ
BY
{ (InstLemma `isolate_summand` [n;f;m] THENA 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 ∈ ℤ))
7. Σ(f[x] | x < n) = (f[m] + Σ(if (x =z m) then 0 else f[x] fi | x < n)) ∈ ℤ
⊢ Σ(f[x] | x < n) = (f[m] + f[k]) ∈ ℤ
Latex:
Latex:
1. n : \mBbbN{}
2. f : \mBbbN{}n {}\mrightarrow{} \mBbbZ{}
3. m : \mBbbN{}n
4. k : \mBbbN{}n
5. \mneg{}(m = k)
6. \mforall{}x:\mBbbN{}n. ((\mneg{}(x = m)) {}\mRightarrow{} (\mneg{}(x = k)) {}\mRightarrow{} (f[x] = 0))
\mvdash{} \mSigma{}(f[x] | x < n) = (f[m] + f[k])
By
Latex:
(InstLemma `isolate\_summand` [n;f;m] THENA Auto)
Home
Index