---

Step * 2 of Lemma qsum-const2

.....falsecase..... 
1. a : ℤ
2. b : ℤ
3. q : ℚ
4. b < a
⊢ Σa ≤ i < b. q = (0 * q) ∈ ℚ
BY
{ xxx((RepUR ``qsum rng_sum mon_itop`` 0 THEN RecUnfold `itop` 0 THEN Reduce 0) THEN SplitOnConclITE THEN Auto')xxx }

---

Latex:

---

Latex:
.....falsecase..... 
1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  q  :  \mBbbQ{}
4.  b  <  a
\mvdash{}  \mSigma{}a  \mleq{}  i  <  b.  q  =  (0  *  q)


By

---

Latex:
xxx((RepUR  ``qsum  rng\_sum  mon\_itop``  0  THEN  RecUnfold  `itop`  0  THEN  Reduce  0)
        THEN  SplitOnConclITE
        THEN  Auto')xxx

---

Home Index