what goes below is not the exact copy of the Mizar article.
I substituted "*" for Extended ASCII \249, "\Sigma" for \228
and "^2" for \253.
As you see the Mizar system is not very good with computation.
This is that should be improved. The length of the proof
depends on the data base (such things as RVSUM_1:80 are refernces
to the facts stored in data base, this one is the reference to
the theorem no. 80 in the article RVSUM_1).
The time of checking - about 2 sec on 486.
=============================================
environ
vocabulary FINSEQ, IDSEQ, SIGMA, RVOP, REAL_1, SQUARE;
constructors RVSUM_1,SQUARE_1,FINSEQOP,NAT_1,REAL_1,NEWTON;
notation ARYTM,REAL_1,NAT_1,SQUARE_1,FINSEQ_1,FINSEQ_2,
FINSEQOP,RVSUM_1,NEWTON;
theorems FINSEQ_2,RVSUM_1,REAL_2,AXIOMS,SQUARE_1,FINSEQOP;
requirements ARYTM;
schemes NAT_1;
begin
for n being Nat holds \Sigma (sqr idseq n) = n*(n+1)*(2*n+1)/6
proof
a: 6 <> 0; then
A: \Sigma (sqr idseq 0) = 0*(0+1)*(2*0+1)/6 by RVSUM_1:80,102,REAL_2:50,FINSEQ_2:58;
B: now let k be Nat;
set s = idseq k, r = k qua Real+1, i = 2*k+1;
assume
C: \Sigma (sqr s) = k*(k+1)*(2*k+1)/6;
b: \Sigma sqr <*r*> = \Sigma <*r^2*> by RVSUM_1:81
.= r^2 by RVSUM_1:103
.= r*r by SQUARE_1:def 3;
t: r*(k*i) = r*k*i & r*(r*6) = r*r*6 by AXIOMS:16;
r: r*(r+1)*(2*r+1) = r*((r+1)*(2*r+1)) by AXIOMS:16
.= r*(r*(2*r+1)+1*(2*r+1)) by AXIOMS:18
.= r*(r*(2*k+2*1+1)+(2*r+1)) by AXIOMS:18
.= r*(r*(i+2)+(2*r+1)) by AXIOMS:13
.= r*(r*i+r*2+(2*r+1)) by AXIOMS:18
.= r*(k*i+1*i+r*2+(2*r+1)) by AXIOMS:18
.= r*(k*i+i+(r*2+(2*r+1))) by AXIOMS:13
.= r*(k*i+(i+(r*2+(r*2+1)))) by AXIOMS:13
.= r*(k*i+(i+(r*2+r*2+1))) by AXIOMS:13
.= r*(k*i+(i+1+(r*2+r*2))) by AXIOMS:13
.= r*(k*i+(2*k+(1+1)*1+(r*2+r*2))) by AXIOMS:13
.= r*(k*i+(r*2+(r*2+r*2))) by AXIOMS:18
.= r*(k*i+(r*2+r*(2+2))) by AXIOMS:18
.= r*(k*i+ r*(2+4)) by AXIOMS:18
.= k*r*i + r*r*6 by t,AXIOMS:18;
A: sqr s = sqrreal*s & sqr <*r*> = sqrreal*<*r*> by RVSUM_1:def 8;
L: sqr(s^<*r*>) = sqrreal*(s^<*r*>) by RVSUM_1:def 8
.= sqr s ^ sqr <*r*> by A,FINSEQOP:10;
idseq(k+1) = s ^ <*r*> by FINSEQ_2:60;
hence \Sigma sqr idseq(k+1) = k*r*i/6 + r*r by C,b,RVSUM_1:105,L
.= (k+1)*((k+1)+1)*(2*(k+1)+1)/6 by r,REAL_2:65,a;
end;
thus thesis from Ind(A,B);
end;