---

Step * of Lemma qsum-reciprocal-squares

∀[J:ℕ+]. (Σ1 ≤ n < J + 1. (1/n * n) ≤ (2 - (1/J)))
BY
{ xxx(Auto
      THEN (NatPlusInd (-1) THENA Auto)
      THEN (RWO "sum_unroll_hi_q" 0 THEN Reduce 0)
      THEN Try (Complete (Auto))
      THEN (Subst' ((J + 1) + 1) - 1 ~ J + 1 0 THENA Auto)
      THEN RWO "-1" 0
      THEN Auto)xxx }

1
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))

---

Latex:

---

Latex:
\mforall{}[J:\mBbbN{}\msupplus{}].  (\mSigma{}1  \mleq{}  n  <  J  +  1.  (1/n  *  n)  \mleq{}  (2  -  (1/J)))


By

---

Latex:
xxx(Auto
        THEN  (NatPlusInd  (-1)  THENA  Auto)
        THEN  (RWO  "sum\_unroll\_hi\_q"  0  THEN  Reduce  0)
        THEN  Try  (Complete  (Auto))
        THEN  (Subst'  ((J  +  1)  +  1)  -  1  \msim{}  J  +  1  0  THENA  Auto)
        THEN  RWO  "-1"  0
        THEN  Auto)xxx

---

Home Index