---

Step * 1 1 1 1 of Lemma rv-sep-exists


1. n : {1...}
⊢ Σ{(r0 - if (i =z 0) then r1 else r0 fi ) * (r0 - if (i =z 0) then r1 else r0 fi ) | 0≤i≤n - 1} = r1
BY
{ ((RWO "rsum-split-first" 0 THENA Auto) THEN Reduce 0) }

1
1. n : {1...}
⊢ (((r0 - r1) * (r0 - r1))
+ Σ{(r0 - if (i =z 0) then r1 else r0 fi ) * (r0 - if (i =z 0) then r1 else r0 fi ) | 1≤i≤n - 1})
= r1

---

Latex:

---

Latex:

1.  n  :  \{1...\}
\mvdash{}  \mSigma{}\{(r0  -  if  (i  =\msubz{}  0)  then  r1  else  r0  fi  )  *  (r0  -  if  (i  =\msubz{}  0)  then  r1  else  r0  fi  )  |  0\mleq{}i\mleq{}n  -  1\}
=  r1


By

---

Latex:
((RWO  "rsum-split-first"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index