---

Step * of Lemma sum-consecutive-squares

∀[n:ℕ]. (Σ(i * i | i < n) = (((n - 1) * n * ((2 * n) - 1)) ÷ 6) ∈ ℤ)
BY
{ (InstLemma `sum-of-consecutive-squares` [] THEN ParallelLast' THEN RevHypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (\mSigma{}(i  *  i  |  i  <  n)  =  (((n  -  1)  *  n  *  ((2  *  n)  -  1))  \mdiv{}  6))


By

---

Latex:
(InstLemma  `sum-of-consecutive-squares`  []  THEN  ParallelLast'  THEN  RevHypSubst'  (-1)  0  THEN  Auto)

---

Home Index