---

Step * 1 of Lemma rsum-constant2


1. n : ℤ
2. m : ℤ
3. a : ℝ
⊢ (a * Σ{r1 | n≤k≤m}) = (a * if m <z n then r0 else r((m - n) + 1) fi )
BY
{ (Unfold `rsum` 0 THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto)))⋅ }

1
1. n : ℤ
2. m : ℤ
3. a : ℝ
⊢ (a * radd-list(map(λk.r1;[n, m + 1)))) = (a * if m <z n then r0 else r((m - n) + 1) fi )

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  a  :  \mBbbR{}
\mvdash{}  (a  *  \mSigma{}\{r1  |  n\mleq{}k\mleq{}m\})  =  (a  *  if  m  <z  n  then  r0  else  r((m  -  n)  +  1)  fi  )


By

---

Latex:
(Unfold  `rsum`  0  THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto)))\mcdot{}

---

Home Index