---

Step * 1 1 1 1 of Lemma approx-ball-to-ball_wf

.....aux..... 
1. n : ℕ
2. k : ℕ+
3. s : ℕn ⟶ {-k..k + 1-}
4. Σ((s i) * (s i) | i < n) ≤ (k * k)
5. Σ{r(s i) * r(s i) | 0≤i≤n - 1} ≤ r(k * k)
6. i : ℤ
7. 0 ≤ i
8. i ≤ (n - 1)
⊢ (r(s i) * r(s i)/r(k) * r(k)) = ((r1/r(k * k)) * r(s i) * r(s i))
BY
{ ((GenConclTerm ⌜r(s i) * r(s i)⌝⋅ THENA Auto)
   THEN All Thin
   THEN (Assert k * k ∈ ℕ+ BY
               Auto)
   THEN RWO "rmul-int" 0
   THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}\msupplus{}
3.  s  :  \mBbbN{}n  {}\mrightarrow{}  \{-k..k  +  1\msupminus{}\}
4.  \mSigma{}((s  i)  *  (s  i)  |  i  <  n)  \mleq{}  (k  *  k)
5.  \mSigma{}\{r(s  i)  *  r(s  i)  |  0\mleq{}i\mleq{}n  -  1\}  \mleq{}  r(k  *  k)
6.  i  :  \mBbbZ{}
7.  0  \mleq{}  i
8.  i  \mleq{}  (n  -  1)
\mvdash{}  (r(s  i)  *  r(s  i)/r(k)  *  r(k))  =  ((r1/r(k  *  k))  *  r(s  i)  *  r(s  i))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}r(s  i)  *  r(s  i)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  (Assert  k  *  k  \mmember{}  \mBbbN{}\msupplus{}  BY
                          Auto)
  THEN  RWO  "rmul-int"  0
  THEN  Auto)

---

Home Index