---

Step * 1 of Lemma qsum-reciprocal-squares


1. J : ℤ
2. 0 < J
3. Σ1 ≤ n < J + 1. (1/n * n) ≤ (2 - (1/J))
⊢ ((2 - (1/J)) + (1/(J + 1) * (J + 1))) ≤ (2 - (1/J + 1))
BY
{ (QMul ⌜J + 1⌝ 0⋅ THEN QMul ⌜J + 1⌝ 0⋅ THEN QMul ⌜J⌝ 0⋅ THEN Repeat ((RWO "qmul-mul qadd-add" 0 THEN Auto))) }

---

Latex:

---

Latex:

1.  J  :  \mBbbZ{}
2.  0  <  J
3.  \mSigma{}1  \mleq{}  n  <  J  +  1.  (1/n  *  n)  \mleq{}  (2  -  (1/J))
\mvdash{}  ((2  -  (1/J))  +  (1/(J  +  1)  *  (J  +  1)))  \mleq{}  (2  -  (1/J  +  1))


By

---

Latex:
(QMul  \mkleeneopen{}J  +  1\mkleeneclose{}  0\mcdot{}
  THEN  QMul  \mkleeneopen{}J  +  1\mkleeneclose{}  0\mcdot{}
  THEN  QMul  \mkleeneopen{}J\mkleeneclose{}  0\mcdot{}
  THEN  Repeat  ((RWO  "qmul-mul  qadd-add"  0  THEN  Auto)))

---

Home Index