---

Step * 1 of Lemma qsum-int

.....assertion..... 
∀d:ℕ. ∀i,j:ℤ.  ((i ≤ j) ⇒ (j ≤ (i + d)) ⇒ (∀X:{i..j-} ⟶ ℤ. (Σi ≤ x < j. X[x] ∈ ℤ)))
BY
{ (InductionOnNat
   THEN Auto
   THEN Try ((RepUR ``qsum rng_sum mon_itop`` 0
              THEN RecUnfold `itop` 0
              THEN SplitOnConclITE
              THEN Auto'
              THEN (Assert False BY
                          Complete (Auto'))
              THEN Auto))⋅) }

1
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-} ⟶ ℤ
⊢ Σi ≤ x < j. X[x] ∈ ℤ

---

Latex:

---

Latex:
.....assertion..... 
\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{})))


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  Try  ((RepUR  ``qsum  rng\_sum  mon\_itop``  0
                        THEN  RecUnfold  `itop`  0
                        THEN  SplitOnConclITE
                        THEN  Auto'
                        THEN  (Assert  False  BY
                                                Complete  (Auto'))
                        THEN  Auto))\mcdot{})

---

Home Index