---

Step * of Lemma frs-non-dec-sum

No Annotations
∀p:ℝ List. (1 < ||p|| ⇒ frs-non-dec(p) ⇒ (Σ{p[i + 1] - p[i] | 0≤i≤||p|| - 2} = (last(p) - p[0])))
BY
{ (InductionOnList THEN Reduce 0 THEN Auto THEN (Decide ⌜1 < ||v||⌝⋅ THENA Auto) THEN ThinTrivial) }

1
1. u : ℝ
2. v : ℝ List
3. 1 < ||v|| + 1
4. frs-non-dec([u / v])
5. 1 < ||v||
6. frs-non-dec(v) ⇒ (Σ{v[i + 1] - v[i] | 0≤i≤||v|| - 2} = (last(v) - v[0]))
⊢ Σ{[u / v][i + 1] - [u / v][i] | 0≤i≤(||v|| + 1) - 2} = (last([u / v]) - u)

2
1. u : ℝ
2. v : ℝ List
3. 1 < ||v|| + 1
4. frs-non-dec([u / v])
5. ¬1 < ||v||
⊢ Σ{[u / v][i + 1] - [u / v][i] | 0≤i≤(||v|| + 1) - 2} = (last([u / v]) - u)

---

Latex:

---

Latex:
No  Annotations
\mforall{}p:\mBbbR{}  List.  (1  <  ||p||  {}\mRightarrow{}  frs-non-dec(p)  {}\mRightarrow{}  (\mSigma{}\{p[i  +  1]  -  p[i]  |  0\mleq{}i\mleq{}||p||  -  2\}  =  (last(p)  -  p[0])))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  (Decide  \mkleeneopen{}1  <  ||v||\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinTrivial)

---

Home Index