---

Step * of Lemma qsum-reciprocal-squares-bound

∀[J:ℕ]. Σ1 ≤ n < J. (1/n * n) < 2
BY
{ (Auto THEN CaseNat 0 `J') }

1
1. J : ℕ
2. J = 0 ∈ ℤ
⊢ Σ1 ≤ n < 0. (1/n * n) < 2

2
1. J : ℕ
2. ¬(J = 0 ∈ ℤ)
⊢ Σ1 ≤ n < J. (1/n * n) < 2

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  CaseNat  0  `J')

---

Home Index