Re: [mizar] Has someone done that?

[Andrzej Trybulec <trybulec@cs.shinshu-u.ac.jp>]

Piotr Rudnicki wrote:

> Peter Koepke from Bonn (koepke@math.uni-bonn.de) wrote me this
>
>         I was in vain looking for a Mizar proof of
>         the summation formula
>
>         $1+2+3+\dots+n = \frac{1}{2}n^2 + \frac{1}{2}n$

I did it often with students, but I cannot find it in MML.

I believe the simple proof is:

 reserve n for Nat;
A: Sum idseq 0 = 0*(0+1)/2 by FINSEQ_2:58,RVSUM_1:102;
B: Sum idseq n = n*(n+1)/2
         implies Sum idseq(n+1) = (n+1)*(n+1+1)/2
   proof assume
B: Sum idseq n = n*(n+1)/2;
    thus Sum idseq(n+1)
             = Sum((idseq n)^<*n+1 qua Real*>) by FINSEQ_2:60
            .= Sum(idseq n) + (n+1) by RVSUM_1:104
            .= n*(n+1)/2 + 2*(n+1)/2 by B,REAL_2:62
            .= (n*(n+1)+(1+1)*(n+1))/2 by REAL_1:40
            .= (n+(1+1))*(n+1)/2 by AXIOMS:18
            .= (n+1)*(n+1+1)/2 by AXIOMS:13;
   end;
  Sum idseq n = n*(n+1)/2 from Ind(A,B);

In the following environment:



>
>
> I vaguely recall that someone (Andrzej?) has proven this some time ago.
> I cannot find it.  AFAIK, Peter would like to have an expository proof
> of it.  I could do it but maybe someone has got it already?
>
> --
> Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
> email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr