Step
*
2
2
of Lemma
qsum-int
1. ∀d:ℕ. ∀i,j:ℤ.  ((i ≤ j) 
⇒ (j ≤ (i + d)) 
⇒ (∀X:{i..j-} ⟶ ℤ. (Σi ≤ x < j. X[x] ∈ ℤ)))
2. i : ℤ
3. j : ℤ
4. X : {i..j-} ⟶ ℤ
5. ¬i < j
⊢ Σi ≤ x < j. X[x] ∈ ℤ
BY
{ xxx(RepUR ``qsum rng_sum mon_itop`` 0 THEN RecUnfold `itop` 0 THEN SplitOnConclITE THEN Auto')xxx }
Latex:
Latex:
1.  \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{})))
2.  i  :  \mBbbZ{}
3.  j  :  \mBbbZ{}
4.  X  :  \{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}
5.  \mneg{}i  <  j
\mvdash{}  \mSigma{}i  \mleq{}  x  <  j.  X[x]  \mmember{}  \mBbbZ{}
By
Latex:
xxx(RepUR  ``qsum  rng\_sum  mon\_itop``  0  THEN  RecUnfold  `itop`  0  THEN  SplitOnConclITE  THEN  Auto')xxx
Home
Index