helphome pageduck scriptspecificationfirst proof pagepage 1 1

Sum of the Squares of the First n Natural Numbers


We want to prove
( N  : Nat  ) 6 * sumsq(N) = (((2 * N) * N) * N) + (((3 * N) * N) + N) .
We use induction on N to prove this goal. For this, we use the induction scheme based on the signature { 0, s } for Nat. Induction requires that we do the following:
  1. Base case: prove the assertion for N = 0 .
    • We show 6 * sumsq(0) = (((2 * 0) * 0) * 0) + (((3 * 0) * 0) + 0) by reduction.
  2. Induction case: assume the assertion for N = N0 , and then prove it for N = s N0 .
    • Quantifier elimination introduces the new constant(s) n0 : Nat  .
    • Implication elimination assumes
          6 * sumsq(n0) = (((2 * n0) * n0) * n0) + (((3 * n0) * n0) + n0) .
    • We show 6 * sumsq(s n0) = (((2 * (s n0)) * (s n0)) * (s n0)) + (((3 * (s n0)) * (s n0)) + (s n0)) by reduction.

And thus the main goal is proved.

BOBJ proof scoreLeft    Up    Down    Right   
 

       This page was generated by Kumo on Tue Feb 13 19:33:24 PST 2001.