Re: [mizar] Has someone done that?

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

I have found my article from 1998. I attach a part of it, where you can
find a proof of the fact.

One remark: right side of the equality is slightly different.

I propose to append this fact to one of the existing MML articles.

Artur

On Fri, 27 Sep 2002, Piotr Rudnicki wrote:

> Hi:
>
> 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 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
>


=======================================

Artur Kornilowicz               e-mail: arturk@math.uwb.edu.pl

Dept. of Applied Logic          http://math.uwb.edu.pl/~arturk/
Institute of Computer Science   fax. +48 (85) 745-7662
University of Bialystok         tel. +48 (85) 745-7559 (office)
Sosnowa 64                           +48 (85) 651-6193 (home)
15-887 Bialystok, Poland

:: Induction ...



environ

 vocabulary FINSEQ_1, FINSEQ_2, ARYTM_3, RLVECT_1, ARYTM;

 notation ARYTM, REAL_1, RVSUM_1, NAT_1, FINSEQ_1, FINSEQ_2, NEWTON;

 constructors NAT_1, FINSEQ_2, NEWTON, RVSUM_1, SQUARE_1, REAL_1, ARYTM;

 theorems AXIOMS, FINSEQ_2, REAL_1, REAL_2, RVSUM_1;

 schemes NAT_1;

 requirements ARYTM, BOOLE, SUBSET, REAL;

 clusters ARYTM, ARYTM_3, NAT_1;



begin

 reserve n for Nat;



theorem Th1:

Sum idseq n = (n * (n + 1)) / 2

 proof:::

A: Sum idseq 0 = (0 * (0 + 1)) / 2 by FINSEQ_2:58, RVSUM_1:102;

B: for n st Sum idseq n = (n * (n+1)) / 2 holds

    Sum idseq (n+1) = ((n+1) * ((n+1) + 1)) / 2

   proof

    let n such that

C:   Sum idseq n = (n * (n+1)) / 2;

    reconsider r = n as Real;

E:  (n*(n+1) + 2*(n+1))/2 = (2*(n+1))/2 + n*(n+1)/2 by REAL_1:40;

    Sum idseq (n+1) = Sum ((idseq n) ^ <*r+1*>) by FINSEQ_2:60

      .= (n * (n+1)) / 2 + (n+1) by C,RVSUM_1:104

      .= (n * (n+1) + 2 * (n+1)) / 2 by REAL_2:62,E

      .= ((n+1) * (n+(1+1))) / 2 by AXIOMS:18;

    hence thesis by AXIOMS:13;

   end;

   for n holds Sum idseq n = (n * (n + 1)) / 2 from Ind(A, B);

   hence thesis;

 end;



theorem

Sum idseq 0 = 0

 proof:::

  thus Sum idseq 0 = (0 * (0 + 1)) / 2 by Th1

   .=0;

 end;



theorem

Sum idseq 1 = 1

 proof:::

  thus Sum idseq 1 = (1 * (1 + 1)) / 2 by Th1

   .= 1;

 end;



theorem

Sum idseq 2 = 3

 proof:::

  thus Sum idseq 2 = (2 * (2 + 1)) / 2 by Th1

   .= 3;

 end;



theorem

Sum idseq 3 = 6

 proof:::

  thus Sum idseq 3 = (3 * (3 + 1)) / 2 by Th1

   .= 6;

 end;