---

Step * 2 2 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 of Lemma real-cube-uniform-continuity


1. n : ℤ
2. i : ℕn
3. v : ℝ^n
4. 2 ≤ n
5. i = 0 ∈ ℤ
6. Σ{if i@0 <z 0 then v i@0 else v (i@0 + 1) fi  * if i@0 <z 0 then v i@0 else v (i@0 + 1) fi  | 0≤i@0≤n - 1 - 1}
= Σ{(v (i + 1)) * (v (i + 1)) | 0≤i≤n - 1 - 1}
7. Σ{(v i) * (v i) | 1≤i≤n - 1} ~ Σ{(v (i + 1)) * (v (i + 1)) | 0≤i≤n - 1 - 1}
8. ∀[x:ℕ(n - 1) + 1 ⟶ ℝ]. Σ{x[i] | 0≤i≤n - 1} = (x[0] + Σ{x[i] | 0 + 1≤i≤n - 1}) supposing 0 ≤ (n - 1)
⊢ Σ{(v i) * (v i) | 1≤i≤n - 1} ≤ (((v 0) * (v 0)) + Σ{(v i) * (v i) | 0 + 1≤i≤n - 1})
BY
{ (Reduce 0 THEN (Assert r0 ≤ ((v 0) * (v 0)) BY Auto) THEN RWO "-1<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  i  :  \mBbbN{}n
3.  v  :  \mBbbR{}\^{}n
4.  2  \mleq{}  n
5.  i  =  0
6.  \mSigma{}\{if  i@0  <z  0  then  v  i@0  else  v  (i@0  +  1)  fi 
*  if  i@0  <z  0  then  v  i@0  else  v  (i@0  +  1)  fi    |  0\mleq{}i@0\mleq{}n  -  1  -  1\}
=  \mSigma{}\{(v  (i  +  1))  *  (v  (i  +  1))  |  0\mleq{}i\mleq{}n  -  1  -  1\}
7.  \mSigma{}\{(v  i)  *  (v  i)  |  1\mleq{}i\mleq{}n  -  1\}  \msim{}  \mSigma{}\{(v  (i  +  1))  *  (v  (i  +  1))  |  0\mleq{}i\mleq{}n  -  1  -  1\}
8.  \mforall{}[x:\mBbbN{}(n  -  1)  +  1  {}\mrightarrow{}  \mBbbR{}]
          \mSigma{}\{x[i]  |  0\mleq{}i\mleq{}n  -  1\}  =  (x[0]  +  \mSigma{}\{x[i]  |  0  +  1\mleq{}i\mleq{}n  -  1\})  supposing  0  \mleq{}  (n  -  1)
\mvdash{}  \mSigma{}\{(v  i)  *  (v  i)  |  1\mleq{}i\mleq{}n  -  1\}  \mleq{}  (((v  0)  *  (v  0))  +  \mSigma{}\{(v  i)  *  (v  i)  |  0  +  1\mleq{}i\mleq{}n  -  1\})


By

---

Latex:
(Reduce  0  THEN  (Assert  r0  \mleq{}  ((v  0)  *  (v  0))  BY  Auto)  THEN  RWO  "-1<"  0  THEN  Auto)

---

Home Index