---

Step * 1 1 2 1 1 2 1 1 of Lemma slln-lemma2

.....assertion..... 
1. B : ℚ
2. n : ℕ
3. 0 ≤ B
4. ¬(n = 0 ∈ ℤ)
⊢ Σ1 ≤ i < n. if (i =z 0) then 0 else (1/i * i) fi  < 2
BY
{ xxx((InstLemma `qsum-reciprocal-squares-bound` [⌜n⌝]⋅ THENA Auto)
      THEN (NthHypEq (-1))
      THEN RepeatFor 2 ((EqCD THEN Auto)))xxx }

---

Latex:

---

Latex:
.....assertion..... 
1.  B  :  \mBbbQ{}
2.  n  :  \mBbbN{}
3.  0  \mleq{}  B
4.  \mneg{}(n  =  0)
\mvdash{}  \mSigma{}1  \mleq{}  i  <  n.  if  (i  =\msubz{}  0)  then  0  else  (1/i  *  i)  fi    <  2


By

---

Latex:
xxx((InstLemma  `qsum-reciprocal-squares-bound`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (NthHypEq  (-1))
        THEN  RepeatFor  2  ((EqCD  THEN  Auto)))xxx

---

Home Index