---

Step * of Lemma qsum-int

∀[i,j:ℤ]. ∀[X:{i..j-} ⟶ ℤ].  (Σi ≤ x < j. X[x] ∈ ℤ)
BY
{ xxxAssert  ⌜∀d:ℕ. ∀i,j:ℤ.  ((i ≤ j) ⇒ (j ≤ (i + d)) ⇒ (∀X:{i..j-} ⟶ ℤ. (Σi ≤ x < j. X[x] ∈ ℤ)))⌝⋅xxx }

1
.....assertion..... 
∀d:ℕ. ∀i,j:ℤ.  ((i ≤ j) ⇒ (j ≤ (i + d)) ⇒ (∀X:{i..j-} ⟶ ℤ. (Σi ≤ x < j. X[x] ∈ ℤ)))

2
1. ∀d:ℕ. ∀i,j:ℤ.  ((i ≤ j) ⇒ (j ≤ (i + d)) ⇒ (∀X:{i..j-} ⟶ ℤ. (Σi ≤ x < j. X[x] ∈ ℤ)))
⊢ ∀[i,j:ℤ]. ∀[X:{i..j-} ⟶ ℤ].  (Σi ≤ x < j. X[x] ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}[i,j:\mBbbZ{}].  \mforall{}[X:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}].    (\mSigma{}i  \mleq{}  x  <  j.  X[x]  \mmember{}  \mBbbZ{})


By

---

Latex:
xxxAssert    \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}i,j:\mBbbZ{}.    ((i  \mleq{}  j)  {}\mRightarrow{}  (j  \mleq{}  (i  +  d))  {}\mRightarrow{}  (\mforall{}X:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}.  (\mSigma{}i  \mleq{}  x  <  j.  X[x]  \mmember{}  \mBbbZ{})))\mkleeneclose{}
\mcdot{}xxx

---

Home Index