---

Step * 1 1 2 of Lemma qsum-int


1. d : ℤ
2. 0 < d
3. ∀i,j:ℤ.  ((i ≤ j) ⇒ (j ≤ (i + (d - 1))) ⇒ (∀X:{i..j-} ⟶ ℤ. (Σi ≤ x < j. X[x] ∈ ℤ)))
4. i : ℤ
5. j : ℤ
6. i ≤ j
7. j ≤ (i + d)
8. X : {i..j-} ⟶ ℤ
9. ¬(i = j ∈ ℤ)
⊢ Σi ≤ x < j. X[x] ∈ ℤ
BY
{ Subst' Σi ≤ x < j. X[x] ~ Σi ≤ x < j - 1. X[x] + X[j - 1] 0⋅ }

1
.....equality..... 
1. d : ℤ
2. 0 < d
3. ∀i,j:ℤ.  ((i ≤ j) ⇒ (j ≤ (i + (d - 1))) ⇒ (∀X:{i..j-} ⟶ ℤ. (Σi ≤ x < j. X[x] ∈ ℤ)))
4. i : ℤ
5. j : ℤ
6. i ≤ j
7. j ≤ (i + d)
8. X : {i..j-} ⟶ ℤ
9. ¬(i = j ∈ ℤ)
⊢ Σi ≤ x < j. X[x] ~ Σi ≤ x < j - 1. X[x] + X[j - 1]

2
1. d : ℤ
2. 0 < d
3. ∀i,j:ℤ.  ((i ≤ j) ⇒ (j ≤ (i + (d - 1))) ⇒ (∀X:{i..j-} ⟶ ℤ. (Σi ≤ x < j. X[x] ∈ ℤ)))
4. i : ℤ
5. j : ℤ
6. i ≤ j
7. j ≤ (i + d)
8. X : {i..j-} ⟶ ℤ
9. ¬(i = j ∈ ℤ)
⊢ Σi ≤ x < j - 1. X[x] + X[j - 1] ∈ ℤ

---

Latex:

---

Latex:

1.  d  :  \mBbbZ{}
2.  0  <  d
3.  \mforall{}i,j:\mBbbZ{}.    ((i  \mleq{}  j)  {}\mRightarrow{}  (j  \mleq{}  (i  +  (d  -  1)))  {}\mRightarrow{}  (\mforall{}X:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}.  (\mSigma{}i  \mleq{}  x  <  j.  X[x]  \mmember{}  \mBbbZ{})))
4.  i  :  \mBbbZ{}
5.  j  :  \mBbbZ{}
6.  i  \mleq{}  j
7.  j  \mleq{}  (i  +  d)
8.  X  :  \{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}
9.  \mneg{}(i  =  j)
\mvdash{}  \mSigma{}i  \mleq{}  x  <  j.  X[x]  \mmember{}  \mBbbZ{}


By

---

Latex:
Subst'  \mSigma{}i  \mleq{}  x  <  j.  X[x]  \msim{}  \mSigma{}i  \mleq{}  x  <  j  -  1.  X[x]  +  X[j  -  1]  0\mcdot{}

---

Home Index