---

Step * of Lemma qsum-const2

∀[a,b:ℤ]. ∀[q:ℚ].  (Σa ≤ i < b. q = (if a ≤z b then b - a else 0 fi  * q) ∈ ℚ)
BY
{ xxx(Auto THEN (SplitOnConclITE THENA Auto))xxx }

1
.....truecase..... 
1. a : ℤ
2. b : ℤ
3. q : ℚ
4. a ≤ b
⊢ Σa ≤ i < b. q = ((b - a) * q) ∈ ℚ

2
.....falsecase..... 
1. a : ℤ
2. b : ℤ
3. q : ℚ
4. b < a
⊢ Σa ≤ i < b. q = (0 * q) ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[q:\mBbbQ{}].    (\mSigma{}a  \mleq{}  i  <  b.  q  =  (if  a  \mleq{}z  b  then  b  -  a  else  0  fi    *  q))


By

---

Latex:
xxx(Auto  THEN  (SplitOnConclITE  THENA  Auto))xxx

---

Home Index