---

Step * 2 1 1 1 of Lemma real-unit-ball-totally-bounded1


1. n : ℕ+
2. k : ℕ+
3. p : ℝ^n
4. ||p|| ≤ r1
5. ∀i:ℕn. ∃z:ℤ. ((|(r(z)/r(k * 8 * n))| ≤ |p i|) ∧ (|(p i) - (r(z)/r(k * 8 * n))| ≤ (r(2)/r(k * 2 * n))))
6. f : i:ℕn ⟶ ℤ
7. ∀i:ℕn. ((|(r(f i)/r(k * 8 * n))| ≤ |p i|) ∧ (|(p i) - (r(f i)/r(k * 8 * n))| ≤ (r(2)/r(k * 2 * n))))
8. x : ℕn
9. |(r(f x)/r(k * 8 * n))| ≤ |p x|
⊢ |p x|^2 ≤ Σ{(p i) * (p i) | 0≤i≤n - 1}
BY
{ Assert ⌜∀a:ℝ. ((a * a) = |a|^2)⌝⋅ }

1
.....assertion..... 
1. n : ℕ+
2. k : ℕ+
3. p : ℝ^n
4. ||p|| ≤ r1
5. ∀i:ℕn. ∃z:ℤ. ((|(r(z)/r(k * 8 * n))| ≤ |p i|) ∧ (|(p i) - (r(z)/r(k * 8 * n))| ≤ (r(2)/r(k * 2 * n))))
6. f : i:ℕn ⟶ ℤ
7. ∀i:ℕn. ((|(r(f i)/r(k * 8 * n))| ≤ |p i|) ∧ (|(p i) - (r(f i)/r(k * 8 * n))| ≤ (r(2)/r(k * 2 * n))))
8. x : ℕn
9. |(r(f x)/r(k * 8 * n))| ≤ |p x|
⊢ ∀a:ℝ. ((a * a) = |a|^2)

2
1. n : ℕ+
2. k : ℕ+
3. p : ℝ^n
4. ||p|| ≤ r1
5. ∀i:ℕn. ∃z:ℤ. ((|(r(z)/r(k * 8 * n))| ≤ |p i|) ∧ (|(p i) - (r(z)/r(k * 8 * n))| ≤ (r(2)/r(k * 2 * n))))
6. f : i:ℕn ⟶ ℤ
7. ∀i:ℕn. ((|(r(f i)/r(k * 8 * n))| ≤ |p i|) ∧ (|(p i) - (r(f i)/r(k * 8 * n))| ≤ (r(2)/r(k * 2 * n))))
8. x : ℕn
9. |(r(f x)/r(k * 8 * n))| ≤ |p x|
10. ∀a:ℝ. ((a * a) = |a|^2)
⊢ |p x|^2 ≤ Σ{(p i) * (p i) | 0≤i≤n - 1}

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  k  :  \mBbbN{}\msupplus{}
3.  p  :  \mBbbR{}\^{}n
4.  ||p||  \mleq{}  r1
5.  \mforall{}i:\mBbbN{}n
          \mexists{}z:\mBbbZ{}.  ((|(r(z)/r(k  *  8  *  n))|  \mleq{}  |p  i|)  \mwedge{}  (|(p  i)  -  (r(z)/r(k  *  8  *  n))|  \mleq{}  (r(2)/r(k  *  2  *  n))))
6.  f  :  i:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
7.  \mforall{}i:\mBbbN{}n
          ((|(r(f  i)/r(k  *  8  *  n))|  \mleq{}  |p  i|)  \mwedge{}  (|(p  i)  -  (r(f  i)/r(k  *  8  *  n))|  \mleq{}  (r(2)/r(k  *  2  *  n))))
8.  x  :  \mBbbN{}n
9.  |(r(f  x)/r(k  *  8  *  n))|  \mleq{}  |p  x|
\mvdash{}  |p  x|\^{}2  \mleq{}  \mSigma{}\{(p  i)  *  (p  i)  |  0\mleq{}i\mleq{}n  -  1\}


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}a:\mBbbR{}.  ((a  *  a)  =  |a|\^{}2)\mkleeneclose{}\mcdot{}

---

Home Index