:: Partial Sum of Some Series
:: by Ming Liang and Yuzhong Ding
::
:: Received September 25, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SEQ_1, COMPLEX1, ARYTM_1, NEWTON, ABIAN, RELAT_1, POWER,
NAT_1, ARYTM_3, REALSET1, XXREAL_0, CARD_1, FUNCT_1, SERIES_1, REAL_1;
notations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, NAT_1, PBOOLE,
NAT_D, SEQ_1, NEWTON, SERIES_1, ABIAN, POWER, XXREAL_0, RELSET_1,
VALUED_0, FUNCT_2;
constructors XXREAL_0, REAL_1, NAT_1, NAT_D, NEWTON, SERIES_1, ABIAN,
VALUED_1, PBOOLE;
registrations XREAL_0, MEMBERED, NEWTON, NUMBERS, RELSET_1, VALUED_0, FUNCT_2,
NAT_1, INT_1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems NEWTON, XCMPLX_1, SERIES_1, NAT_1, POWER, ABSVALUE, XREAL_1,
WSIERP_1, PEPIN, XXREAL_0;
schemes NAT_1;
begin
reserve n for Nat,
a,b for Real,
s for Real_Sequence;
theorem Th1:
|.(-1)|^n.| = 1
proof
per cases;
suppose
A1: n is even;
(-1)|^n =(-1) to_power n by POWER:41
.=1 to_power n by A1,POWER:47
.=1 by POWER:26;
hence thesis by ABSVALUE:def 1;
end;
suppose
A2: n is odd;
(-1)|^n =(-1) to_power n by POWER:41
.=-(1 to_power n) by A2,POWER:48
.=-1 by POWER:26;
then |.(-1)|^n.|=--1 by ABSVALUE:def 1;
hence thesis;
end;
end;
Lm1: a|^3=a*a*a
proof
a|^(2+1)=a|^2*a by NEWTON:6;
hence thesis by WSIERP_1:1;
end;
Lm2: a|^3=a|^2*a
proof
a|^(2+1) = a|^2*a by NEWTON:6;
hence thesis;
end;
Lm3: 4=2|^2 & (a+b)|^2=a|^2+2*a*b+b|^2
proof
A1: (a+b)|^(1+1) = (a+b)|^1*(a+b) by NEWTON:6
.= (a+b)*(a+b)
.=(a*a+a*b)+(a*b+b*b)
.=(a*a+a*b)+(a*b+b|^2) by WSIERP_1:1
.=(a|^2+a*b)+(a*b+b|^2) by WSIERP_1:1
.=a|^2+2*(a*b)+b|^2;
2|^2= 2*2 by WSIERP_1:1
.=4;
hence thesis by A1;
end;
Lm4: (a+1)|^3 = a|^3+3*a|^2+3*a+1
proof
(a+1)|^3 = ((a+1)|^2)*(a+1) by Lm2
.=(a|^2+2*a*1+1|^2)*(a+1) by Lm3
.=(a|^2+2*a+1)*(a+1)
.=a|^2*a+a|^2*1+(2*a*a+2*a)+(1*a+1*1)
.=a|^2*a+a|^2*1+(2*a*a+2*a*1)+(1|^2*a+1)
.=a|^(2+1)+a|^2+(2*a*a+2*a)+(1|^2*a+1) by NEWTON:6
.=a|^3+a|^2+(2*(a*a)+2*a)+(1*a+1)
.=a|^3+a|^2+(2*(a|^1*a)+2*a)+(a+1)
.=a|^3+a|^2+(2*a|^(1+1)+2*a)+(a+1) by NEWTON:6
.=a|^3+a|^2+2*a|^2+2*a+(a+1);
hence thesis;
end;
Lm5: n*(2*n+1)*(3*n|^2+3*n-1)+(n+1)|^3*30 = (n+2)*(2*(n+1)+1)*(3*(n+1)|^2+3*(n
+1)-1)
proof
(n+2)*(2*(n+1)+1)*(3*(n+1)|^2+3*(n+1)-1) =(n+2)*(2*n+3)*(3*(n|^2+2*n*1+1
|^2)+(3*n+3)-1) by Lm3
.=((n*(2*n)+2*(2*n))+(n*3+2*3))*(3*(n|^2+2*n+1|^2)+3*n+3-1)
.=((n*(2*n)+2*(2*n))+(n*3+2*3))*(3*(n|^2+2*n+1)+3*n+3-1)
.=((n*n*2+2*2*n)+(n*3+6))*((n|^2*3+6*n+3)+3*n+3-1)
.=(2*n|^2+4*n+(n*3+6))*(3*n|^2+6*n+3+3*n+3-1) by WSIERP_1:1
.=2*(n|^2*n|^2)*3+2*n|^2*n*9+10*n|^2+(7*n*n|^2*3+7*n*n*9+35*n) +(6*3*n|^
2+6*9*n+30)
.=2*n|^(2+2)*3+2*(n|^2*n)*9+10*n|^2+(7*(n*n|^2)*3+7*(n*n)*9+35*n) +(18*n
|^2+54*n+30) by NEWTON:8
.=2*n|^4*3+2*n|^(2+1)*9+10*n|^2+(7*(n*n|^2)*3+7*(n*n)*9+35*n) +(18*n|^2+
54*n+30) by NEWTON:6
.=6*n|^4+2*n|^3*9+10*n|^2+(7*n|^(2+1)*3+7*(n*n)*9+35*n) +(18*n|^2+54*n+
30) by NEWTON:6;
then
A1: (n+2)*(2*(n+1)+1)*(3*(n+1)|^2+3*(n+1)-1) =6*n|^4+18*n|^3+10*n|^2+(7*n|^3
*3+7*n|^2*9+35*n) +(18*n|^2+54*n+30) by WSIERP_1:1
.=6*n|^4+39*n|^3+(73+18)*n|^2+89*n+30;
n*(2*n+1)*(3*n|^2+3*n-1) + (n+1)|^3*30 =(2*(n*n)+n)*(3*n|^2+3*n-1) + (n+
1)|^3*30
.=(2*(n|^1*n)+n)*(3*n|^2+3*n-1) + (n+1)|^3*30
.=(2*(n|^(1+1))+n)*(3*n|^2+3*n-1) + (n+1)|^3*30 by NEWTON:6
.=2*(n|^2*n|^2)*3+n*n|^2*3+(2*(n|^2*n)*3+n*n*3)-(2*n|^2+n)+(n+1)|^3*30
.=2*n|^(2+2)*3+n*n|^2*3+(2*(n|^2*n)*3+n*n*3)-(2*n|^2+n)+(n+1)|^3*30 by
NEWTON:8
.=2*n|^4*3+n*n|^2*3+(2*(n|^(2+1))*3+n*n*3)-(2*n|^2+n)+(n+1)|^3*30 by
NEWTON:6
.=2*n|^4*3+n*n|^2*3+(2*n|^3*3+n|^2*3)-(2*n|^2+n)+(n+1)|^3*30 by WSIERP_1:1
.=6*n|^4+n|^(2+1)*3+(6*n|^3+n|^2*3)-(2*n|^2+n)+(n+1)|^3*30 by NEWTON:6
.=6*n|^4+9*n|^3+1*n|^2-n+(n|^3+3*n|^2+3*n+1)*30 by Lm4
.=6*n|^4+39*n|^3+91*n|^2+(90-1)*n+30;
hence thesis by A1;
end;
Lm6: for n being Real holds (n+1)|^4=n|^4+4*n|^3+6*n|^2+4*n+1 & (n+1)|^
5=n|^5+5*n|^4+10*n|^3+10*n|^2+5*n+1
proof
let n be Real;
A1: (n+1)|^(3+1)=(n+1)|^3*(n+1) by NEWTON:6
.=(n|^3+3*n|^2+3*n+1)*(n+1) by Lm4
.=n|^3*n+n|^3+(3*(n|^2*n)+3*n|^2)+(3*(n*n)+3*n)+(n+1)
.=n|^(3+1)+n|^3+(3*(n|^2*n)+3*n|^2)+(3*(n*n)+3*n)+(n+1) by NEWTON:6
.=n|^(3+1)+n|^3+(3*n|^(2+1)+3*n|^2)+(3*(n*n)+3*n)+(n+1) by NEWTON:6
.=n|^4+n|^3+(3*n|^3+3*n|^2)+(3*n|^2+3*n)+(n+1) by WSIERP_1:1;
(n+1)|^(3+2)=(n+1)|^3*(n+1)|^2 by NEWTON:8
.=(n|^3+3*n|^2+3*n+1)*(n+1)|^2 by Lm4
.=(n|^3+3*n|^2+3*n+1)*(n|^2+2*n*1+1|^2) by Lm3
.=(n|^3+3*n|^2+3*n+1)*(n|^2+2*n+1)
.=(n|^3*n|^2+2*n*n|^3+n|^3*1)+(3*n|^2*n|^2+2*n*(3*n|^2)+3*n|^2*1) +(3*n*
n|^2+3*n*(2*n)+3*n*1)+(n|^2+2*n+1)
.=(n|^(3+2)+2*(n*n|^3)+n|^3)+(3*(n|^2*n|^2)+2*(n*n|^2)*3+3*n|^2) +(3*(n*
n|^2)+3*(n*n)*2+3*n)+(n|^2+2*n+1) by NEWTON:8
.=(n|^(3+2)+2*(n*n|^3)+n|^3)+(3*n|^(2+2)+2*(n*n|^2)*3+3*n|^2) +(3*(n*n|^
2)+3*(n*n)*2+3*n)+(n|^2+2*n+1) by NEWTON:8
.=(n|^(3+2)+2*n|^(3+1)+n|^3)+(3*n|^(2+2)+2*(n*n|^2)*3+3*n|^2) +(3*(n*n|^
2)+3*(n*n)*2+3*n)+(n|^2+2*n+1) by NEWTON:6
.=(n|^(3+2)+2*n|^(3+1)+n|^3)+(3*n|^(2+2)+2*n|^(2+1)*3+3*n|^2) +(3*(n*n|^
2)+3*(n*n)*2+3*n)+(n|^2+2*n+1) by NEWTON:6
.=(n|^5+2*n|^4+n|^3)+(3*n|^4+2*n|^3*3+3*n|^2) +(3*n|^3+3*(n*n)*2+3*n)+(n
|^2+2*n+1) by NEWTON:6
.=(n|^5+2*n|^4+n|^3)+(3*n|^4+6*n|^3+3*n|^2)+(3*n|^3+3*n|^2*2+3*n) +(n|^2
+2*n+1) by WSIERP_1:1;
hence thesis by A1;
end;
theorem
for n being Real holds (n+1)|^3=n|^3+3*n|^2+3*n+1 & (n+1)|^4=n
|^4+4*n|^3+6*n|^2+4*n+1 & (n+1)|^5=n|^5+5*n|^4+10*n|^3+10*n|^2+5*n+1 by Lm4,Lm6
;
Lm7: for n holds 1-1/(n+2)=(n+1)/(n+2) & 1/((n+1)!) = (n+2)/(((n+1)!)*(n+2))
proof
let n;
n>=0 by NAT_1:2;
then n+1>0 by NAT_1:13;
then
A1: n+1+1>0 by NAT_1:13;
then
A2: 1/((n+1)!)=(1*(n+2))/(((n+1)!)*(n+2)) by XCMPLX_1:91;
(n+1)/(n+2)=(n+2-1)/(n+2) .=(n+2)/(n+2)-1/(n+2) by XCMPLX_1:120
.=1-1/(n+2) by A1,XCMPLX_1:60;
hence thesis by A2;
end;
Lm8: 1/(n+1)-2/((n+1)*(n+3))=1/(n+3)
proof
n>=0 by NAT_1:2;
then
A1: n+1>0 by NAT_1:13;
then n+1+1>0 by NAT_1:13;
then n+2+1>0 by NAT_1:13;
then 1/(n+1)-2/((n+1)*(n+3)) =1*(n+3)/((n+1)*(n+3))-2/((n+1)*(n+3)) by
XCMPLX_1:91
.=(n+3-2)/((n+1)*(n+3)) by XCMPLX_1:120
.=(n+1)*1/((n+1)*(n+3))
.=1/(n+3) by A1,XCMPLX_1:91;
hence thesis;
end;
Lm9: 1/(n+1)-3/((n+1)*(n+4))=1/(n+4)
proof
n>=0 by NAT_1:2;
then
A1: n+1>0 by NAT_1:13;
then n+1+1>0 by NAT_1:13;
then n+2+1>0 by NAT_1:13;
then n+3+1>0 by NAT_1:13;
then 1/(n+1)-3/((n+1)*(n+4)) =1*(n+4)/((n+1)*(n+4))-3/((n+1)*(n+4)) by
XCMPLX_1:91
.=(n+4-3)/((n+1)*(n+4)) by XCMPLX_1:120
.=(n+1)*1/((n+1)*(n+4))
.=1/(n+4) by A1,XCMPLX_1:91;
hence thesis;
end;
Lm10: n|^2+3*n+2 = (n+1)*(n+2)
proof
(n+1)*(n+2)=n*n+(2*n+1*n)+2 .= n|^1*n+(2+1)*n+2
.= n|^(1+1)+(2+1)*n+2 by NEWTON:6;
hence thesis;
end;
Lm11: n*(4*n|^2) + 11*n + 12*n|^2+3 = (n+1)*(4*(n+1)|^2-1)
proof
(n+1)*(4*(n+1)|^2-1) = (n+1)*(4*(n|^2+2*n*1+1|^2)-1) by Lm3
.= (n+1)*(4*(n|^2+2*n+1)-1)
.= n*(4*n|^2)+4*n|^2+(8*(n*n)+8*n)+(3*n+3*1)
.= n*(4*n|^2)+4*n|^2+(8*n|^2+8*n)+(3*n+3*1) by WSIERP_1:1
.= n*(4*n|^2)+(4*n|^2+8*n|^2)+(8*n+3*n)+3;
hence thesis;
end;
Lm12: (n+1)|^2*(2*(n+1)|^2-1)=n|^2*n|^2*2+(12-1)*n|^2 + 8*n|^3+6*n+1
proof
(n+1)|^2*(2*(n+1)|^2-1) = (n+1)|^2*(2*(n+1)|^2)-(n+1)|^2*1
.=(n+1)|^2*(n+1)|^2*2-(n|^2+2*n*1+1|^2) by Lm3
.=(n+1)|^2*(n+1)|^2*2-(n|^2+2*n+1)
.=(n+1)|^2*(n|^2+2*n*1+1|^2)*2-(n|^2+2*n+1) by Lm3
.=(n|^2+2*n*1+1|^2)*(n|^2+2*n+1|^2)*2-(n|^2+2*n+1) by Lm3
.=(n|^2+2*n+1|^2)*(n|^2+2*n+1)*2-(n|^2+2*n+1)
.=(n|^2+2*n+1)*(n|^2+2*n+1)*2-(n|^2+2*n+1)
.=(n|^2*n|^2+2*n*n|^2+n|^2+(2*n*n|^2+2*n*n*2+2*n)+(n|^2+2*n+1))*2 -(n|^2
+2*n+1)
.=(n|^2*n|^2+2*(n|^(2+1))+n|^2+(2*(n*n|^2)+2*(n*n)*2+2*n)+(n|^2+2*n+1))*
2 -(n|^2+2*n+1) by NEWTON:6
.=(n|^2*n|^2+2*(n|^(2+1))+n|^2+(2*(n|^(2+1))+2*(n*n)*2+2*n)+(n|^2+2*n+1)
)*2 -(n|^2+2*n+1) by NEWTON:6
.=(n|^2*n|^2+2*n|^3+n|^2+(2*n|^3+2*(n|^1*n)*2+2*n)+(n|^2+2*n+1))*2 -(n|^
2+2*n+1)
.=(n|^2*n|^2+2*n|^3+n|^2+(2*n|^3+2*n|^(1+1)*2+2*n)+(n|^2+2*n+1))*2 -(n|^
2+2*n+1) by NEWTON:6
.=(n|^2*n|^2+2*n|^3+n|^2+(2*n|^3+2*n|^2*2+2*n)+(n|^2+2*n+1))*2 -(n|^2+2*
n+1);
hence thesis;
end;
Lm13: (n+2)*((n+1)|^2+(n+1)-1)=n|^3+5*n|^2+7*n+2
proof
(n+2)*((n+1)|^2+(n+1)-1) =(n+2)*(n|^2+2*n*1+1|^2+(n+1)-1) by Lm3
.=(n+2)*(n|^2+2*n*1+1+(n+1)-1)
.=n*n|^2+2*n|^2+3*(n*n)+6*n+n+2
.=n*n|^2+2*n|^2+3*n|^2+6*n+n+2 by WSIERP_1:1
.=n|^(2+1)+2*n|^2+3*n|^2+6*n+n+2 by NEWTON:6
.=n|^(2+1)+(2+3)*n|^2+(6+1)*n+2;
hence thesis;
end;
Lm14: (for n holds s.n = a*n+b) implies for n holds Partial_Sums(s).n = a*(n+1
)*n/2+n*b+b
proof
defpred X[Nat] means Partial_Sums(s).$1 = a*($1+1)*$1/2+$1*b+b;
assume
A1: for n holds s.n = a*n+b;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = a*(n+1)*n/2+n*b+b;
then Partial_Sums(s).(n+1) = a*(n+1)*n/2+n*b+b+s.(n+1) by SERIES_1:def 1
.=a*(n+1)*n/2+n*b+b + (a*(n+1)+b) by A1
.=a*(n+1)*(n+2)/2+(n+1)*b+b;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.= a*(0+1)*0/2+0*b+b by A1;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = n) implies for n holds Partial_Sums(s).n = n*(n+1)/ 2
proof
defpred X[Nat] means Partial_Sums(s).$1 = $1*($1+1)/2;
assume
A1: for n holds s.n = n;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = n*(n+1)/2;
then Partial_Sums(s).(n+1) = n*(n+1)/2 + s.(n+1) by SERIES_1:def 1
.=n*(n+1)/2 + (n+1) by A1
.=(n*(n+1) + (n+1)*2)/2;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0*(0+1)/2 by A1;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = 2*n) implies for n holds Partial_Sums(s).n = n*(n+1 )
proof
defpred X[Nat] means Partial_Sums(s).$1 = $1*($1+1);
assume
A1: for n holds s.n = 2*n;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = n*(n+1);
then Partial_Sums(s).(n+1) = n*(n+1) + s.(n+1) by SERIES_1:def 1
.=n*(n+1) + 2*(n+1) by A1
.=(n + 2)*(n+1);
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=2*0 by A1
.= 0*(0+1);
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = 2*n+1) implies for n holds Partial_Sums(s).n = (n+1 )|^2
proof
defpred X[Nat] means Partial_Sums(s).$1 = ($1+1)|^2;
assume
A1: for n holds s.n = 2*n+1;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = (n+1)|^2;
then Partial_Sums(s).(n+1) = (n+1)|^2 + s.(n+1) by SERIES_1:def 1
.=(n+1)|^2 + (2*(n+1)+1) by A1
.=(n+1)|^2 +2*n+3
.= n|^2+2*n*1+1|^2+2*n+3 by Lm3
.= n|^2+2*n+1+2*n+3
.= n|^2+2*n*2+2|^2 by Lm3
.= (n+2)|^2 by Lm3;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=2*0+1 by A1
.= (0+1)|^2;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = n*(n+1)) implies for n holds Partial_Sums(s).n = n*
(n+1)*(n+2)/3
proof
defpred X[Nat] means Partial_Sums(s).$1 = $1*($1+1)*($1+2)/3;
assume
A1: for n holds s.n = n*(n+1);
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = n*(n+1)*(n+2)/3;
then Partial_Sums(s).(n+1) = n*(n+1)*(n+2)/3 + s.(n+1) by SERIES_1:def 1
.=n*(n+1)*(n+2)/3 + (n+1)*(n+1+1) by A1
.=(n+1)*(n+2)*(n+3)/3;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0*(0+1)*(0+2)/3 by A1;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = n*(n+1)*(n+2)) implies for n holds Partial_Sums(s).
n = n*(n+1)*(n+2)*(n+3)/4
proof
defpred X[Nat] means Partial_Sums(s).$1 = $1*($1+1)*($1+2)*($1+3)
/4;
assume
A1: for n holds s.n = n*(n+1)*(n+2);
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n =n*(n+1)*(n+2)*(n+3)/4;
then Partial_Sums(s).(n+1) = n*(n+1)*(n+2)*(n+3)/4 + s.(n+1) by
SERIES_1:def 1
.=n*(n+1)*(n+2)*(n+3)/4+ (n+1)*(n+1+1)*(n+1+2) by A1
.=(n+1)*(n+1+1)*(n+1+2)*(n+1+3)/4;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0*(0+1)*(0+2)*(0+3)/4 by A1;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = n*(n+1)*(n+2)*(n+3)) implies for n holds
Partial_Sums(s).n = n*(n+1)*(n+2)*(n+3)*(n+4)/5
proof
defpred X[Nat] means Partial_Sums(s).$1 = $1*($1+1)*($1+2)*($1+3)
*($1+4)/5;
assume
A1: for n holds s.n = n*(n+1)*(n+2)*(n+3);
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n =n*(n+1)*(n+2)*(n+3)*(n+4)/5;
then Partial_Sums(s).(n+1) = n*(n+1)*(n+2)*(n+3)*(n+4)/5 + s.(n+1) by
SERIES_1:def 1
.=n*(n+1)*(n+2)*(n+3)*(n+4)/5+ (n+1)*(n+1+1)*(n+1+2)*(n+1+3) by A1
.=(n+1)*(n+2)*(n+3)*(n+4)*(n+5)/5;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0*(0+1)*(0+2)*(0+3)*(0+4)/4 by A1;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = 1/(n*(n+1))) implies for n holds Partial_Sums(s).n
= 1-1/(n+1)
proof
defpred X[Nat] means Partial_Sums(s).$1 = 1-1/($1+1);
assume
A1: for n holds s.n = 1/(n*(n+1));
A2: for n st X[n] holds X[n+1]
proof
let n;
A3: n+1<>0 by NAT_1:5;
assume Partial_Sums(s).n =1-1/(n+1);
then Partial_Sums(s).(n+1) = 1-1/(n+1) + s.(n+1) by SERIES_1:def 1
.=1-1/(n+1) + 1/((n+1)*(n+1+1)) by A1
.=1-(1/(n+1) - 1/((n+1)*(n+2)))
.=1-(1*(1/(n+1)) - (1/(n+1))*(1/(n+2))) by XCMPLX_1:102
.=1-1/(n+1)*(1 - 1/(n+2))
.=1-1/(n+1)*((1*(n+2)-1)/(n+2)) by Lm7
.=1-(1/(n+1)*(n+1))/(n+2) by XCMPLX_1:74
.=1-1/(n+2) by A3,XCMPLX_1:87;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=1/(0*(0+1)) by A1
.=1-1/1 by XCMPLX_1:49;
then
A4: X[0];
for n holds X[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem
(for n holds s.n = 1/(n*(n+1)*(n+2))) implies for n holds Partial_Sums
(s).n = 1/4-1/(2*(n+1)*(n+2))
proof
defpred X[Nat] means Partial_Sums(s).$1 =1/4-1/(2*($1+1)*($1+2));
assume
A1: for n holds s.n = 1/(n*(n+1)*(n+2));
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n =1/4-1/(2*(n+1)*(n+2));
then Partial_Sums(s).(n+1) =1/4-1/(2*(n+1)*(n+2))+ s.(n+1) by
SERIES_1:def 1
.=1/4-1/(2*(n+1)*(n+2))+1/((n+1)*(n+1+1)*(n+1+2)) by A1
.=1/4-(1/((2*(n+1))*(n+2))-1/((n+1)*(n+2)*(n+3)))
.=1/4-(1/((2*(n+2))*(n+1))-(1*2)/((n+2)*(n+1)*(n+3)*2)) by XCMPLX_1:91
.=1/4-(1/((2*(n+2))*(n+1))-(1*2)/((n+2)*2*((n+1)*(n+3))))
.=1/4-(1/((2*(n+2))*(n+1))-1/((n+2)*2)*(2/((n+1)*(n+3)))) by XCMPLX_1:76
.=1/4-(1/(2*(n+2))*(1/(n+1))-1/(2*(n+2))*(2/((n+1)*(n+3)))) by
XCMPLX_1:102
.=1/4-1/(2*(n+2))*(1/(n+1)-2/((n+1)*(n+3)))
.=1/4-1/(2*(n+2))*(1/(n+3)) by Lm8
.=1/4-1/(2*(n+1+1)*(n+1+2)) by XCMPLX_1:102;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=1/(0*(0+1)*(0+2)) by A1
.=1/4-1/(2*(0+1)*(0+2)) by XCMPLX_1:49;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = 1/(n*(n+1)*(n+2)*(n+3))) implies for n holds
Partial_Sums(s).n = 1/18-1/(3*(n+1)*(n+2)*(n+3))
proof
defpred X[Nat] means Partial_Sums(s).$1 = 1/18-1/(3*($1+1)*($1+2)
*($1+3));
assume
A1: for n holds s.n = 1/(n*(n+1)*(n+2)*(n+3));
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = 1/18-1/(3*(n+1)*(n+2)*(n+3));
then Partial_Sums(s).(n+1) =1/18-1/(3*(n+1)*(n+2)*(n+3)) + s.(n+1) by
SERIES_1:def 1
.=1/18-1/(3*(n+1)*(n+2)*(n+3)) +1/((n+1)*(n+1+1)*(n+1+2)*(n+1+3)) by A1
.=1/18-(1/(3*(n+1)*(n+2)*(n+3))-1/((n+1)*(n+2)*(n+3)*(n+4)))
.=1/18-(1/(3*(n+1)*(n+2)*(n+3))-(1*3)/((n+1)*(n+2)*(n+3)*(n+4)*3)) by
XCMPLX_1:91
.=1/18-(1/((3*(n+2)*(n+3))*(n+1))-1*3/((3*(n+2)*(n+3))*((n+1)*(n+4))))
.=1/18-(1/((3*(n+2)*(n+3))*(n+1))-1/(3*(n+2)*(n+3))*(3/((n+1)*(n+4))))
by XCMPLX_1:76
.=1/18-(1/(3*(n+2)*(n+3))*(1/(n+1))-1/(3*(n+2)*(n+3))*(3/((n+1)*(n+4))
)) by XCMPLX_1:102
.=1/18-1/(3*(n+2)*(n+3))*(1/(n+1)-3/((n+1)*(n+4)))
.=1/18-1/(3*(n+2)*(n+3))*(1/(n+4)) by Lm9
.=1/18-1/(3*(n+1+1)*(n+1+2)*(n+1+3)) by XCMPLX_1:102;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.= 1/(0*(0+1)*(0+2)*(0+3)) by A1
.=1/18-1/(3*(0+1)*(0+2)*(0+3)) by XCMPLX_1:49;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = n |^ 2) implies for n holds Partial_Sums(s).n = n*(
n+1)*(2*n+1)/6
proof
defpred X[Nat] means Partial_Sums(s).$1 = $1*($1+1)*(2*$1+1)/6;
assume
A1: for n holds s.n = n |^ 2;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = n*(n+1)*(2*n+1)/6;
then Partial_Sums(s).(n+1) = n*(n+1)*(2*n+1)/6 + s.(n+1) by SERIES_1:def 1
.=n*(n+1)*(2*n+1)/6 + (n+1) |^ 2 by A1
.=(n*(n+1)*(2*n+1) + ((n+1) |^ 2)*6)/6
.=((n+1)*n*(2*n+1) + (n+1)*(n+1)*6)/6 by WSIERP_1:1;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0 |^2 by A1
.=0*(0+1)*(2*0+1)/6 by NEWTON:11;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = (-1)|^(n+1)*n|^2) implies for n holds Partial_Sums(
s).n = (-1)|^(n+1)*n*(n+1)/2
proof
defpred X[Nat] means Partial_Sums(s).$1 = (-1)|^($1+1)*$1*($1+1)/
2;
assume
A1: for n holds s.n = (-1)|^(n+1)*n|^2;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = (-1)|^(n+1)*n*(n+1)/2;
then Partial_Sums(s).(n+1) = (-1)|^(n+1)*n*(n+1)/2 + s.(n+1) by
SERIES_1:def 1
.=(-1)|^(n+1)*n*(n+1)/2 + (-1)|^(n+1+1)*(n+1)|^2 by A1
.=((-1)|^(n+1)*n*(n+1) + (-1)|^(n+1+1)*(n+1)|^2*2)/2
.=((-1)|^(n+1)*n*(n+1) + (-1)|^(n+1)*(-1)*(n+1)|^2*2)/2 by NEWTON:6
.=((-1)|^(n+1)*(-1)*((-1)*(n*(n+1))+(n+1)|^2*2))/2
.=((-1)|^(n+1+1)*((-1)*(n*(n+1))+(n+1)|^2*2))/2 by NEWTON:6
.=((-1)|^(n+2)*((-1)*n*n+(-1)*n*1+(n|^2+2*n*1+1|^2 )*2))/2 by Lm3
.=((-1)|^(n+2)*((-1)*n*n+(-1)*n*1+(n|^2+2*n+1)*2))/2
.=((-1)|^(n+2)*((-1)*(n*n)+(-1)*n+(2*n|^2+2*n*2+1*2)))/2
.=((-1)|^(n+2)*((-1)*(n|^1*n)+(-1)*n+(2*n|^2+2*n*2+1*2)))/2
.=((-1)|^(n+2)*((-1)*n|^(1+1)+(-1)*n+(2*n|^2+2*n*2+1*2)))/2 by NEWTON:6
.=((-1)|^(n+2)*(1*n|^2+3*n+2))/2
.=(-1)|^(n+2)*((n+1)*(n+2))/2 by Lm10
.=(-1)|^(n+2)*(n+1)*(n+2)/2;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=(-1)|^(0+1)*0|^2 by A1
.=(-1)|^(0+1)*0*(0+1)/2 by NEWTON:11;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n = (2*n-1)|^2 & s.0 = 0) implies for n st n>=1
holds Partial_Sums(s).n = n*(4*n|^2-1)/3
proof
defpred X[Nat] means Partial_Sums(s).$1 = $1*(4*$1|^2-1)/3;
assume
A1: for n st n>=1 holds s.n = (2*n-1)|^2 & s.0 = 0;
A2: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A3: Partial_Sums(s).n = n*(4*n|^2-1)/3;
A4: n+1>=1 by NAT_1:11;
Partial_Sums(s).(n+1) =n*(4*n|^2-1)/3 + s.(n+1) by A3,SERIES_1:def 1
.=n*(4*n|^2-1)/3 + (2*(n+1)-1)|^2 by A1,A4
.=(n*(4*n|^2-1) + (2*n+1)|^2*3)/3
.=(n*(4*n|^2-1) + ((2*n)|^2+2*(2*n)*1+1|^2)*3)/3 by Lm3
.=(n*4*n|^2-n*1 + ((2*n)|^2*3+2*(2*n)*3+1|^2*3))/3
.=(n*(4*n|^2)-n + ((2|^2*n|^2)*3+2*2*n*3+1|^2*3))/3 by NEWTON:7
.=(n*(4*n|^2)-n + ((2|^2*n|^2)*3+4*n*3+1*3))/3
.=(n*(4*n|^2)-n + ((2*2*n|^2)*3+12*n+3))/3 by WSIERP_1:1
.=(n*(4*n|^2) + (12-1)*n + 12*n|^2+3)/3
.=(n+1)*(4*(n+1)|^2-1)/3 by Lm11;
hence thesis;
end;
Partial_Sums(s).(0+1) = Partial_Sums(s).0 + s.(0+1) by SERIES_1:def 1
.=s.0 + s.1 by SERIES_1:def 1
.=0 + s.1 by A1
.= 0 + (2*1-1)|^2 by A1
.=1*(4*(1*1)-1)/3
.= 1*(4*1|^2-1)/3;
then
A5: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A5,A2);
hence thesis;
end;
theorem
(for n holds s.n = n |^ 3) implies for n holds Partial_Sums(s).n = n|^
2*(n+1)|^2/4
proof
defpred X[Nat] means Partial_Sums(s).$1 = $1|^2*($1+1)|^2/4;
assume
A1: for n holds s.n = n |^ 3;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = n|^2*(n+1)|^2/4;
then Partial_Sums(s).(n+1) = n|^2*(n+1)|^2/4 + s.(n+1) by SERIES_1:def 1
.=n|^2*(n+1)|^2/4 + (n+1) |^ 3 by A1
.=(n|^2*(n+1)|^2 + ((n+1) |^ 3)*4)/4
.=(n|^2*(n+1)|^2 + (n+1)|^2*(n+1)*4)/4 by Lm2
.=(n+1)|^2*(n|^2 +(2*2*n+4))/4
.=(n+1)|^2*(n+2)|^2/4 by Lm3;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0 |^3 by A1
.=0*(0+1)|^2/4 by NEWTON:11
.=0|^2*(0+1)|^2/4 by NEWTON:11;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n = (2*n-1) |^ 3 & s.0 = 0) implies for n st n
>=1 holds Partial_Sums(s).n = n|^2*(2*n|^2-1)
proof
defpred X[Nat] means Partial_Sums(s).$1 = $1|^2*(2*$1|^2-1);
assume
A1: for n st n>=1 holds s.n = (2*n-1) |^ 3 & s.0 = 0;
A2: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A3: Partial_Sums(s).n = n|^2*(2*n|^2-1);
A4: n+1>=1 by NAT_1:11;
Partial_Sums(s).(n+1) = n|^2*(2*n|^2-1) + s.(n+1) by A3,SERIES_1:def 1
.=n|^2*(2*n|^2-1) + (2*(n+1)-1) |^ 3 by A1,A4
.=n|^2*(2*n|^2-1) + (2*n+1) |^3
.=n|^2*(2*n|^2-1) + ((2*n)|^3+3*(2*n)|^2+3*(2*n)+1) by Lm4
.=n|^2*2*n|^2-n|^2 + (2*n)|^3+3*(2*n)|^2+3*2*n+1
.=n|^2*2*n|^2-n|^2 + (2*n)|^3+3*(2|^2*n|^2)+6*n+1 by NEWTON:7
.=n|^2*2*n|^2-n|^2 + 2|^3*n|^3+3*(2|^2*n|^2)+6*n+1 by NEWTON:7
.=n|^2*2*n|^2-n|^2 + 2|^3*n|^3+3*(2*2*n|^2)+6*n+1 by WSIERP_1:1
.=n|^2*2*n|^2-n|^2 + 2*2*2*n|^3+3*(2*2*n|^2)+6*n+1 by Lm1
.=n|^2*n|^2*2+(12-1)*n|^2 + 8*n|^3+6*n+1
.=(n+1)|^2*(2*(n+1)|^2-1) by Lm12;
hence thesis;
end;
Partial_Sums(s).(1+0) =Partial_Sums(s).0 + s.(1+0) by SERIES_1:def 1
.=s.0 + s.1 by SERIES_1:def 1
.=s.1 + 0 by A1
.= (2*1-1)|^3 by A1
.=1|^(2+1)
.=1|^2*(2*(1*1)-1)
.=1|^2*(2*1|^2-1);
then
A5: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A5,A2);
hence thesis;
end;
theorem
(for n holds s.n = n |^ 4) implies for n holds Partial_Sums(s).n = n*(
n+1)*(2*n+1)*(3*n|^2+3*n-1)/30
proof
defpred X[Nat] means Partial_Sums(s).$1=$1*($1+1)*(2*$1+1)*(3*$1
|^2+3*$1-1)/30;
assume
A1: for n holds s.n = n |^ 4;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = n*(n+1)*(2*n+1)*(3*n|^2+3*n-1)/30;
then
Partial_Sums(s).(n+1) =n*(n+1)*(2*n+1)*(3*n|^2+3*n-1)/30 + s.(n+1) by
SERIES_1:def 1
.=n*(n+1)*(2*n+1)*(3*n|^2+3*n-1)/30 + (n+1)|^4 by A1
.=(n*(n+1)*(2*n+1)*(3*n|^2+3*n-1)+ (n+1)|^(3+1)*30)/30
.=(n*(n+1)*(2*n+1)*(3*n|^2+3*n-1)+ (n+1)|^3*(n+1)*30)/30 by NEWTON:6
.=(n+1)*(n*(2*n+1)*(3*n|^2+3*n-1)+ (n+1)|^3*30)/30
.=(n+1)*((n+2)*(2*(n+1)+1)*(3*(n+1)|^2+3*(n+1)-1))/30 by Lm5;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0 |^4 by A1
.=0*(0+1)*(2*0+1)*(3*0|^2+3*0-1)/30 by NEWTON:11;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = (-1)|^(n+1)*n|^4) implies for n holds Partial_Sums(
s).n = (-1)|^(n+1)*n*(n+1)*(n|^2+n-1)/2
proof
defpred X[Nat] means Partial_Sums(s).$1=(-1)|^($1+1)*$1*($1+1)*(
$1|^2+$1-1)/2;
assume
A1: for n holds s.n = (-1)|^(n+1)*n|^4;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = (-1)|^(n+1)*n*(n+1)*(n|^2+n-1)/2;
then Partial_Sums(s).(n+1) =(-1)|^(n+1)*n*(n+1)*(n|^2+n-1)/2 + s.(n+1) by
SERIES_1:def 1
.=(-1)|^(n+1)*n*(n+1)*(n|^2+n-1)/2 + (-1)|^(n+1+1)*(n+1)|^4 by A1
.=((-1)|^(n+1)*(-1)*(-1)*n*(n+1)*(n|^2+n-1) + (-1)|^(n+2)*(n+1)|^4*2)/
2
.=((-1)|^(n+1+1)*(-1)*n*(n+1)*(n|^2+n-1)+(-1)|^(n+2)*(n+1)|^4*2)/2 by
NEWTON:6
.=(-1)|^(n+2)*((-1)*n*(n+1)*(n|^2+n-1)+(n+1)|^(3+1)*2)/2
.=(-1)|^(n+2)*((-1)*n*(n+1)*(n|^2+n-1)+(n+1)|^3*(n+1)*2)/2 by NEWTON:6
.=(-1)|^(n+2)*(n+1)*((-1)*(n*n|^2+n*n-n*1)+(n+1)|^3*2)/2
.=(-1)|^(n+2)*(n+1)*((-1)*(n|^(2+1)+n*n-n*1)+(n+1)|^3*2)/2 by NEWTON:6
.=(-1)|^(n+2)*(n+1)*((-1)*(n|^3+n|^2-n)+(n+1)|^3*2)/2 by WSIERP_1:1
.=(-1)|^(n+2)*(n+1)*((-1)*(n|^3+n|^2-n)+(n|^3+3*n|^2+3*n+1)*2)/2 by Lm4
.=(-1)|^(n+2)*(n+1)*(n|^3+5*n|^2+7*n+2)/2
.=(-1)|^(n+2)*(n+1)*((n+2)*((n+1)|^2+(n+1)-1))/2 by Lm13
.=(-1)|^(n+2)*(n+1)*(n+2)*((n+1)|^2+(n+1)-1)/2;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=(-1)|^(0+1)*0 |^4 by A1
.=(-1)|^(0+1)*0*(0+1)*(0|^2+0-1)/2 by NEWTON:11;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
Lm15: n|^2*(2*n|^2+2*n-1)+(n+1)|^3*12=(n+2)|^2*(2*(n+1)|^2+2*(n+1)-1)
proof
A1: n|^2*(2*n|^2+2*n-1)+(n+1)|^3*12 =(2*(n|^2*n|^2)+2*(n*n|^2)-n|^2)+(n+1)|^
3*12
.=(2*n|^(2+2)+2*(n*n|^2)-n|^2)+(n+1)|^3*12 by NEWTON:8
.=(2*n|^(2+2)+2*n|^(2+1)-n|^2)+(n+1)|^3*12 by NEWTON:6
.=(2*n|^4+2*n|^3-n|^2)+(n|^3+3*n|^2+3*n+1)*12 by Lm4
.=2*n|^4+2*n|^3-n|^2+n|^3*12+36*n|^2+36*n+12;
(n+2)|^2*(2*(n+1)|^2+2*(n+1)-1) =(n+2)|^2*(2*(n|^2+2*n*1+1|^2)+2*(n+1)-1
) by Lm3
.=(n|^2+2*n*2+2|^2)*(2*n|^2+2*n*2+2*1|^2+(2*n+2*1)-1) by Lm3
.=(n|^2+2*n*2+2|^2)*(2*n|^2+4*n+2*1+(2*n+2)-1)
.=(n|^2+4*n+2*2)*(2*n|^2+4*n+2+2*n+2-1) by WSIERP_1:1
.=2*(n|^2*n|^2)+6*(n*n|^2)+n|^2*3+4*n*(2*n|^2+6*n+3)+(2*n|^2*4+24*n+12)
.=2*n|^(2+2)+6*(n*n|^2)+n|^2*3+4*n*(2*n|^2+6*n+3)+(2*n|^2*4+24*n+12) by
NEWTON:8
.=2*n|^(2+2)+6*n|^(2+1)+n|^2*3+4*n*(2*n|^2+6*n+3)+(2*n|^2*4+24*n+12) by
NEWTON:6
.=2*n|^4+6*n|^3+n|^2*3+(4*(n*n|^2)*2+4*(n*n)*6+4*n*3)+(8*n|^2+24*n+12)
.=2*n|^4+6*n|^3+n|^2*3+(4*n|^(2+1)*2+24*(n*n)+4*n*3)+(8*n|^2+24*n+12) by
NEWTON:6
.=2*n|^4+6*n|^3+n|^2*3+(4*n|^3*2+24*n|^2+12*n)+(8*n|^2+24*n+12) by
WSIERP_1:1
.=2*n|^4+14*n|^3+27*n|^2+12*n+8*n|^2+24*n+12;
hence thesis by A1;
end;
theorem
(for n holds s.n = n|^5) implies for n holds Partial_Sums(s).n = n|^2*
(n+1)|^2*(2*n|^2+2*n-1)/12
proof
defpred X[Nat] means Partial_Sums(s).$1=$1|^2*($1+1)|^2*(2*$1|^2+
2*$1-1)/12;
assume
A1: for n holds s.n = n|^5;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = n|^2*(n+1)|^2*(2*n|^2+2*n-1)/12;
then Partial_Sums(s).(n+1) =n|^2*(n+1)|^2*(2*n|^2+2*n-1)/12 + s.(n+1) by
SERIES_1:def 1
.=n|^2*(n+1)|^2*(2*n|^2+2*n-1)/12 + (n+1)|^5 by A1
.=(n|^2*(n+1)|^2*(2*n|^2+2*n-1)+(n+1)|^(3+2)*12)/12
.=(n|^2*(n+1)|^2*(2*n|^2+2*n-1)+(n+1)|^3*(n+1)|^2*12)/12 by NEWTON:8
.=((n+1)|^2*(n|^2*(2*n|^2+2*n-1)+(n+1)|^3*12))/12
.=((n+1)|^2*((n+2)|^2*(2*(n+1)|^2+2*(n+1)-1)))/12 by Lm15
.=(n+1)|^2*(n+2)|^2*(2*(n+1)|^2+2*(n+1)-1)/12;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0 |^5 by A1
.=0*(0+1)|^2*(2*0|^2+2*0-1)/12 by NEWTON:11
.= 0|^2*(0+1)|^2*(2*0|^2+2*0-1)/12 by NEWTON:11;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
Lm16: (n+2)*(2*(n+1)+1)*(3*(n+1)|^4+6*(n+1)|^3-3*(n+1)+1)= 6*n|^6+57*n|^5+216*
n|^4+414*n|^3+419*n|^2+211*n+42
proof
(n+2)*(2*(n+1)+1)*(3*(n+1)|^4+6*(n+1)|^3-3*(n+1)+1) =(n+2)*(2*n+3)*(3*(n
+1)|^4+6*(n+1)|^3-3*n-2)
.=(n+2)*(2*n+3)*(3*(n|^4+4*n|^3+6*n|^2+4*n+1)+6*(n+1)|^3-3*n-2) by Lm6
.=(n+2)*(2*n+3)*(3*n|^4+12*n|^3+18*n|^2+12*n+3+6*(n|^3+3*n|^2+3*n+1)-3*n
-2) by Lm4
.=((2*(n*n)+3*n)+(4*n+6))*(3*n|^4+18*n|^3+36*n|^2+27*n+7)
.=((2*n|^2+3*n)+(4*n+6))*(3*n|^4+18*n|^3+36*n|^2+27*n+7) by WSIERP_1:1
.=(3*n|^4*(2*n|^2+7*n+6)+18*n|^3*(2*n|^2+7*n+6)+36*n|^2*(2*n|^2+7*n+6))
+(27*(n*n|^2)*2+27*(n*n)*7+162*n)+(14*n|^2+49*n+42)
.=(3*n|^4*(2*n|^2+7*n+6)+18*n|^3*(2*n|^2+7*n+6)+36*n|^2*(2*n|^2+7*n+6))
+(27*n|^(2+1)*2+27*(n*n)*7+162*n)+(14*n|^2+49*n+42) by NEWTON:6
.=(3*n|^4*(2*n|^2+7*n+6)+18*n|^3*(2*n|^2+7*n+6)+36*n|^2*(2*n|^2+7*n+6))
+(54*n|^3+27*n|^2*7+162*n)+(14*n|^2+49*n+42) by WSIERP_1:1
.=(3*(n|^4*n|^2)*2+3*(n|^4*n)*7+18*n|^4+(18*(n|^3*n|^2)*2+18*(n|^3*n)*7
+108*n|^3)+36*n|^2*(2*n|^2+7*n+6))+(54*n|^3+203*n|^2+211*n+42)
.=(3*n|^(4+2)*2+3*(n|^4*n)*7+18*n|^4+(18*(n|^3*n|^2)*2+18*(n|^3*n)*7+108
* n|^3)+36*n|^2*(2*n|^2+7*n+6))+(54*n|^3+203*n|^2+211*n+42) by NEWTON:8
.=(6*n|^(4+2)+3*n|^(4+1)*7+18*n|^4+(36*(n|^3*n|^2)+126*(n|^3*n)+108*n|^3
)+ 36*n|^2*(2*n|^2+7*n+6))+(54*n|^3+203*n|^2+211*n+42) by NEWTON:6
.=(6*n|^(4+2)+21*n|^(4+1)+18*n|^4+(36*(n|^3*n|^2)+126*n|^(3+1)+108*n|^3)
+ 36*n|^2*(2*n|^2+7*n+6))+(54*n|^3+203*n|^2+211*n+42) by NEWTON:6
.=(6*n|^(4+2)+21*n|^(4+1)+18*n|^4+(36*n|^(3+2)+126*n|^(3+1)+108*n|^3)+
36*n|^2*(2*n|^2+7*n+6))+(54*n|^3+203*n|^2+211*n+42) by NEWTON:8
.=(6*n|^6+21*n|^5+18*n|^4+(36*n|^5+126*n|^4+108*n|^3)+(36*(n|^2*n|^2)*2
+36*(n|^2*n)*7+216*n|^2))+(54*n|^3+203*n|^2+211*n+42)
.=(6*n|^6+21*n|^5+18*n|^4+(36*n|^5+126*n|^4+108*n|^3)+(36*n|^(2+2)*2 +
252*(n|^2*n)+216*n|^2))+(54*n|^3+203*n|^2+211*n+42) by NEWTON:8
.=(6*n|^6+21*n|^5+18*n|^4+(36*n|^5+126*n|^4+108*n|^3)+(72*n|^(2+2) +252*
n|^(2+1)+216*n|^2))+(54*n|^3+203*n|^2+211*n+42) by NEWTON:6
.=(6*n|^6+21*n|^5+18*n|^4+(36*n|^5+126*n|^4+108*n|^3)+(72*n|^4 +252*n|^3
+216*n|^2))+(54*n|^3+203*n|^2+211*n+42);
hence thesis;
end;
theorem
(for n holds s.n = n|^6) implies for n holds Partial_Sums(s).n = n*(n+
1)*(2*n+1)*(3*n|^4+6*n|^3-3*n+1)/42
proof
defpred X[Nat] means Partial_Sums(s).$1=$1*($1+1)*(2*$1+1)*(3*$1
|^4+6*$1|^3-3*$1+1)/42;
assume
A1: for n holds s.n = n|^6;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = n*(n+1)*(2*n+1)*(3*n|^4+6*n|^3-3*n+1)/42;
then
Partial_Sums(s).(n+1) =n*(n+1)*(2*n+1)*(3*n|^4+6*n|^3-3*n+1)/42+s.(n+1
) by SERIES_1:def 1
.=n*(n+1)*(2*n+1)*(3*n|^4+6*n|^3-3*n+1)/42+(n+1)|^6 by A1
.=(n*(n+1)*(2*n+1)*(3*n|^4+6*n|^3-3*n+1)+(n+1)|^(5+1)*42)/42
.=(n*(n+1)*(2*n+1)*(3*n|^4+6*n|^3-3*n+1)+(n+1)|^5*(n+1)*42)/42 by
NEWTON:6
.=(n+1)*((2*(n*n)+n)*(3*n|^4+6*n|^3-3*n+1)+(n+1)|^5*42)/42
.=(n+1)*((2*n|^2+n)*(3*n|^4+6*n|^3-3*n+1)+(n+1)|^5*42)/42 by WSIERP_1:1
.=(n+1)*(3*(n|^4*n|^2)*2+3*(n|^4*n)+(6*(n|^3*n|^2)*2+6*(n|^3*n)) -(3*(
n*n|^2)*2+3*(n*n))+(2*n|^2+n)+(n+1)|^5*42)/42
.=(n+1)*(3*n|^(4+2)*2+3*(n|^4*n)+(6*(n|^3*n|^2)*2+6*(n|^3*n)) -(3*(n*n
|^2)*2+3*(n*n))+(2*n|^2+n)+(n+1)|^5*42)/42 by NEWTON:8
.=(n+1)*(3*n|^(4+2)*2+3*(n|^4*n)+(6*n|^(3+2)*2+6*(n|^3*n)) -(3*(n*n|^2
)*2+3*(n*n))+(2*n|^2+n)+(n+1)|^5*42)/42 by NEWTON:8
.=(n+1)*(3*n|^(4+2)*2+3*n|^(4+1)+(6*n|^(3+2)*2+6*(n|^3*n)) -(3*(n*n|^2
)*2+3*(n*n))+(2*n|^2+n)+(n+1)|^5*42)/42 by NEWTON:6
.=(n+1)*(3*n|^(4+2)*2+3*n|^(4+1)+(6*n|^(3+2)*2+6*(n|^3*n)) -(3*n|^(2+1
)*2+3*(n*n))+(2*n|^2+n)+(n+1)|^5*42)/42 by NEWTON:6
.=(n+1)*(3*n|^6*2+3*n|^5+(6*n|^5*2+6*(n|^3*n)) -(3*n|^3*2+3*n|^2)+(2*n
|^2+n)+(n+1)|^5*42)/42 by WSIERP_1:1
.=(n+1)*(6*n|^6+3*n|^5+(12*n|^5+6*n|^(3+1)) -(6*n|^3+3*n|^2)+(2*n|^2+n
)+(n+1)|^5*42)/42 by NEWTON:6
.=(n+1)*(6*n|^6+6*n|^4+15*n|^5-6*n|^3-1*n|^2+n+(n|^5+5*n|^4+10*n|^3 +
10*n|^2+5*n+1)*42)/42 by Lm6
.=(n+1)*(6*n|^6+57*n|^5+216*n|^4+414*n|^3+419*n|^2+211*n+42)/42
.=(n+1)*((n+2)*(2*(n+1)+1)*(3*(n+1)|^4+6*(n+1)|^3-3*(n+1)+1))/42 by Lm16
.=(n+1)*(n+1+1)*(2*(n+1)+1)*(3*(n+1)|^4+6*(n+1)|^3-3*(n+1)+1)/42;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0 |^6 by A1
.= 0*(0+1)*(2*0+1)*(3*0|^4+6*0|^3-3*0+1)/42 by NEWTON:11;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
Lm17: (n+2)|^2*(3*(n+1)|^4+6*(n+1)|^3-(n+1)|^2-4*(n+1)+2) =n|^2*(3*n|^4+6*n|^3
-n|^2-4*n+2)+ (n+1)|^5*24
proof
A1: n|^2*(3*n|^4+6*n|^3-n|^2-4*n+2)+ (n+1)|^5*24 =3*(n|^4*n|^2)+6*(n|^3*n|^2
)-n|^2*n|^2-4*(n*n|^2)+n|^2*2+ (n+1)|^5*24
.=3*n|^(4+2)+6*(n|^3*n|^2)-n|^2*n|^2-4*(n*n|^2)+n|^2*2+ (n+1)|^5*24 by
NEWTON:8
.=3*n|^(4+2)+6*n|^(3+2)-n|^2*n|^2-4*(n*n|^2)+n|^2*2+ (n+1)|^5*24 by
NEWTON:8
.=3*n|^(4+2)+6*n|^(3+2)-n|^(2+2)-4*(n*n|^2)+n|^2*2+ (n+1)|^5*24 by NEWTON:8
.=3*n|^(4+2)+6*n|^(3+2)-n|^(2+2)-4*n|^(2+1)+n|^2*2+ (n+1)|^5*24 by NEWTON:6
.=3*n|^6+6*n|^5-n|^4-4*n|^3+n|^2*2+(n|^5+5*n|^4+10*n|^3+10*n|^2+5*n+1)*
24 by Lm6
.=3*n|^6+30*n|^5+119*n|^4+236*n|^3+n|^2*242+120*n+24;
(n+2)|^2*(3*(n+1)|^4+6*(n+1)|^3-(n+1)|^2-4*(n+1)+2) =(n+2)|^2*(3*(n+1)|^
4+6*(n+1)|^3-(n+1)|^2-4*n-4+2)
.=(n+2)|^2*(3*(n+1)|^4+6*(n+1)|^3-(n|^2+2*n*1+1|^2)-4*n-4+2) by Lm3
.=(n+2)|^2*(3*(n+1)|^4+6*(n+1)|^3-(n|^2+2*n*1+1|^2)-4*n-2)
.=(n+2)|^2*(3*(n+1)|^4+6*(n|^3+3*n|^2+3*n+1)-(n|^2+2*n+1|^2)-4*n-2) by Lm4
.=(n+2)|^2*(3*(n+1)|^4+6*(n|^3+3*n|^2+3*n+1)-(n|^2+2*n+1)-4*n-2)
.=(n+2)|^2*(3*(n+1)|^4+6*n|^3+(18-1)*n|^2+(18-2-4)*n+3)
.=(n+2)|^2*(3*(n|^4+4*n|^3+6*n|^2+4*n+1)+6*n|^3+17*n|^2+12*n+3) by Lm6
.=(n|^2+2*n*2+2*2)*(3*n|^4+18*n|^3+35*n|^2+24*n+6) by Lm3
.=3*(n|^4*n|^2)+18*(n|^3*n|^2)+35*(n|^2*n|^2)+24*(n*n|^2)+n|^2*6+4*n*(3
*n|^4+18*n|^3+35*n|^2+24*n+6)+((12*n|^4+72*n|^3+140*n|^2)+96*n+24)
.=3*n|^(4+2)+18*(n|^3*n|^2)+35*(n|^2*n|^2)+24*(n*n|^2)+n|^2*6+4*n*(3*n|^
4+ 18*n|^3+35*n|^2+24*n+6)+((12*n|^4+72*n|^3+140*n|^2)+96*n+24) by NEWTON:8
.=3*n|^(4+2)+18*n|^(3+2)+35*(n|^2*n|^2)+24*(n*n|^2)+n|^2*6+4*n*(3*n|^4+
18*n|^3+35*n|^2+24*n+6)+((12*n|^4+72*n|^3+140*n|^2)+96*n+24) by NEWTON:8
.=3*n|^(4+2)+18*n|^(3+2)+35*n|^(2+2)+24*(n*n|^2)+n|^2*6+4*n*(3*n|^4+ 18*
n|^3+35*n|^2+24*n+6)+((12*n|^4+72*n|^3+140*n|^2)+96*n+24) by NEWTON:8
.=3*n|^(4+2)+18*n|^(3+2)+35*n|^(2+2)+24*n|^(2+1)+n|^2*6+4*n*(3*n|^4+ 18*
n|^3+35*n|^2+24*n+6)+((12*n|^4+72*n|^3+140*n|^2)+96*n+24) by NEWTON:6
.=3*n|^6+18*n|^5+35*n|^4+24*n|^3+n|^2*6+(12*(n|^4*n)+72*(n|^3*n)+140*(n
|^2 *n)+96*(n*n)+24*n)+((12*n|^4+72*n|^3+140*n|^2)+96*n+24)
.=3*n|^6+18*n|^5+35*n|^4+24*n|^3+n|^2*6+(12*n|^(4+1)+72*(n|^3*n)+140*(n
|^2 *n)+96*(n*n)+24*n)+((12*n|^4+72*n|^3+140*n|^2)+96*n+24) by NEWTON:6
.=3*n|^6+18*n|^5+35*n|^4+24*n|^3+n|^2*6+(12*n|^(4+1)+72*n|^(3+1)+140*(n
|^2 *n)+96*(n*n)+24*n)+((12*n|^4+72*n|^3+140*n|^2)+96*n+24) by NEWTON:6
.=3*n|^6+18*n|^5+35*n|^4+24*n|^3+n|^2*6+(12*n|^(4+1)+72*n|^(3+1)+140*n|^
(2 +1)+96*(n*n)+24*n)+((12*n|^4+72*n|^3+140*n|^2)+96*n+24) by NEWTON:6
.=3*n|^6+18*n|^5+35*n|^4+24*n|^3+n|^2*6+(12*n|^5+72*n|^4+140*n|^3+96*n|^
2 +24*n)+((12*n|^4+72*n|^3+140*n|^2)+96*n+24) by WSIERP_1:1
.=3*n|^6+30*n|^5+119*n|^4+236*n|^3+242*n|^2+120*n+24;
hence thesis by A1;
end;
Lm18: 2|^(n+2)+(-1)|^(n+2)>0
proof
A1: (-1)|^(n+2) = |.(-1)|^(n+2).| or -(-1)|^(n+2) = |.(-1)|^(n+2).| by
ABSVALUE:1;
A2: |.(-1)|^(n+2).| = 1 by Th1;
n+2>=2 by NAT_1:11;
then n+2 > 0 by XXREAL_0:2;
then 2|^(n+2) > 1 by PEPIN:25;
then
A3: 2|^(n+2)+(-1)|^(n+2)>1+(-1)|^(n+2) by XREAL_1:8;
per cases by A2,A1;
suppose
(-1)|^(n+2) = -1;
hence thesis by A3;
end;
suppose
(-1)|^(n+2) = 1;
hence thesis by A3,XXREAL_0:2;
end;
end;
Lm19: 2|^(n+3)+(-1)|^(n+3)>0
proof
A1: (-1)|^(n+3) = |.(-1)|^(n+3).| or -(-1)|^(n+3) = |.(-1)|^(n+3).| by
ABSVALUE:1;
A2: |.(-1)|^(n+3).| = 1 by Th1;
n+3>=3 by NAT_1:11;
then n+3 > 0 by XXREAL_0:2;
then 2|^(n+3) > 1 by PEPIN:25;
then
A3: 2|^(n+3)+(-1)|^(n+3)>1+(-1)|^(n+3) by XREAL_1:8;
per cases by A2,A1;
suppose
(-1)|^(n+3) = -1;
hence thesis by A3;
end;
suppose
(-1)|^(n+3) = 1;
hence thesis by A3,XXREAL_0:2;
end;
end;
theorem
(for n holds s.n = n|^7) implies for n holds Partial_Sums(s).n = n|^2*
(n+1)|^2*(3*n|^4+6*n|^3-n|^2-4*n+2)/24
proof
defpred X[Nat] means Partial_Sums(s).$1=$1|^2*($1+1)|^2*(3*$1|^4+
6*$1|^3-$1|^2-4*$1+2)/24;
assume
A1: for n holds s.n = n|^7;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n =n|^2*(n+1)|^2*(3*n|^4+6*n|^3-n|^2-4*n+2)/24;
then
Partial_Sums(s).(n+1) =n|^2*(n+1)|^2*(3*n|^4+6*n|^3-n|^2-4*n+2)/24+ s.
(n+1) by SERIES_1:def 1
.=n|^2*(n+1)|^2*(3*n|^4+6*n|^3-n|^2-4*n+2)/24+ (n+1)|^7 by A1
.=(n|^2*(n+1)|^2*(3*n|^4+6*n|^3-n|^2-4*n+2)+ (n+1)|^(5+2)*24)/24
.=(n|^2*(n+1)|^2*(3*n|^4+6*n|^3-n|^2-4*n+2)+ (n+1)|^5*(n+1)|^2*24)/24
by NEWTON:8
.=(n+1)|^2*(n|^2*(3*n|^4+6*n|^3-n|^2-4*n+2)+ (n+1)|^5*24)/24
.=(n+1)|^2*((n+2)|^2*(3*(n+1)|^4+6*(n+1)|^3-(n+1)|^2-4*(n+1)+2))/24 by
Lm17
.=(n+1)|^2*(n+1+1)|^2*(3*(n+1)|^4+6*(n+1)|^3-(n+1)|^2-4*(n+1)+2)/24;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0 |^7 by A1
.= 0*(0+1)|^2*(3*0|^4+6*0|^3-0|^2-4*0+2)/24 by NEWTON:11
.= 0|^2*(0+1)|^2*(3*0|^4+6*0|^3-0|^2-4*0+2)/24 by NEWTON:11;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = n*(n+1)|^2) implies for n holds Partial_Sums(s).n =
n*(n+1)*(n+2)*(3*n+5)/12
proof
defpred X[Nat] means Partial_Sums(s).$1=$1*($1+1)*($1+2)*(3*$1+5)
/12;
assume
A1: for n holds s.n = n*(n+1)|^2;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n =n*(n+1)*(n+2)*(3*n+5)/12;
then Partial_Sums(s).(n+1) =n*(n+1)*(n+2)*(3*n+5)/12+ s.(n+1) by
SERIES_1:def 1
.=n*(n+1)*(n+2)*(3*n+5)/12+ (n+1)*(n+1+1)|^2 by A1
.=(n+1)*(n*(n+2)*(3*n+5)+ (n+2)|^2*12)/12
.=(n+1)*(n*(n+2)*(3*n+5)+ (n+2)*(n+2)*12)/12 by WSIERP_1:1
.=(n+1)*(n+2)*(n+3)*(3*(n+1)+5)/12;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0*(0+1)|^2 by A1
.=0*(0+1)*(0+2)*(3*0+5)/12;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = n*(n+1)|^2*(n+2)) implies for n holds Partial_Sums(
s).n = n*(n+1)*(n+2)*(n+3)*(2*n+3)/10
proof
defpred X[Nat] means Partial_Sums(s).$1=$1*($1+1)*($1+2)*($1+3)*(
2*$1+3)/10;
assume
A1: for n holds s.n =n*(n+1)|^2*(n+2);
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n =n*(n+1)*(n+2)*(n+3)*(2*n+3)/10;
then Partial_Sums(s).(n+1) =n*(n+1)*(n+2)*(n+3)*(2*n+3)/10+ s.(n+1) by
SERIES_1:def 1
.=n*(n+1)*(n+2)*(n+3)*(2*n+3)/10+ (n+1)*(n+1+1)|^2*(n+1+2) by A1
.=n*(n+1)*(n+2)*(n+3)*(2*n+3)/10+ (n+1)*((n+2)*(n+2))*(n+3)*10/10 by
WSIERP_1:1
.=(n+1)*(n+2)*(n+3)*(n+4)*(2*(n+1)+3)/10;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0*(0+1)|^2*(0+2) by A1
.=0*(0+1)*(0+2)*(0+3)*(2*0+3)/10;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n holds s.n = n*(n+1)*2|^n) implies for n holds Partial_Sums(s).n
= 2|^(n+1)*(n|^2-n+2)-4
proof
defpred X[Nat] means Partial_Sums(s).$1=2|^($1+1)*($1|^2-$1+2)-4;
assume
A1: for n holds s.n = n*(n+1)*2|^n;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = 2|^(n+1)*(n|^2-n+2)-4;
then Partial_Sums(s).(n+1) =2|^(n+1)*(n|^2-n+2)-4 + s.(n+1) by
SERIES_1:def 1
.=2|^(n+1)*(n|^2-n+2)-4 + (n+1)*(n+1+1)*2|^(n+1) by A1
.=2|^(n+1)*2*((n|^2-n+2) + (n+1)*(n+2))/2-4
.=2|^(n+1+1)*((n|^2-n+2) + (n+1)*(n+2))/2-4 by NEWTON:6
.=2|^(n+2)*(n|^2-n+2 + n*n+1*n+n*2+2)/2-4
.=2|^(n+2)*(n|^2-n+2 + n|^2+1*n+n*2+2)/2-4 by WSIERP_1:1
.=2|^(n+2)*(n|^2 + 2*n +1-1- n + 2)-4
.=2|^(n+2)*(n|^2 + 2*n*1 +1|^2-1- n + 2)-4
.=2|^(n+2)*((n+1)|^2-1- n + 2)-4 by Lm3
.=2|^(n+2)*((n+1)|^2-(1+ n) + 2)-4;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.= 0*(0+1)*2|^0 by A1
.=2*2-4
.=2|^(0+1)*(0-0+2)-4
.=2|^(0+1)*(0|^2-0+2)-4 by NEWTON:11;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n = 1/((n-1)*(n+1)) & s.0=0) implies for n st n
>=2 holds Partial_Sums(s).n = 3/4-1/(2*n)-1/(2*(n+1))
proof
defpred X[Nat] means Partial_Sums(s).$1=3/4-1/(2*$1)-1/(2*($1+1));
assume
A1: for n st n>=1 holds s.n = 1/((n-1)*(n+1)) & s.0 = 0;
then
A2: s.1 = 1/((1-1)*(1+1)) .= 0 by XCMPLX_1:49;
A3: for n be Nat st n>=2 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
A4: n>=2 and
A5: Partial_Sums(s).n = 3/4-1/(2*n)-1/(2*(n+1));
A6: n>0 by A4,XXREAL_0:2;
then
A7: n+1>1 by XREAL_1:29;
A8: n+2>=n by NAT_1:11;
Partial_Sums(s).(n+1) = 3/4-1/(2*n)-1/(2*(n+1)) + s.(n+1) by A5,
SERIES_1:def 1
.=3/4-1/(2*n)-1/(2*(n+1))+1/((n+1-1)*(n+1+1)) by A1,A7
.=3/4-1/(2*(n+1))+(1/(n*(n+2))-1/(2*n))
.=3/4-1/(2*(n+1))+(1/(n*(n+2))-1/2*(1/n)) by XCMPLX_1:102
.=3/4-1/(2*(n+1))+(1/n*(1/(n+2))-1/2*(1/n)) by XCMPLX_1:102
.=3/4-1/(2*(n+1))+(1/(n+2)-1/2)*(1/n)
.=3/4-1/(2*(n+1))+(1*2-1*(n+2))/((n+2)*2)*(1/n) by A6,A8,XCMPLX_1:130
.=3/4-1/(2*(n+1))+(-n)/n*(1/((n+2)*2)) by XCMPLX_1:85
.=3/4-1/(2*(n+1))+(-1)*(1/((n+2)*2)) by A6,XCMPLX_1:197
.=3/4-1/(2*(n+1))+-(1/(2*(n+1+1)));
hence thesis;
end;
Partial_Sums(s).(1+1) =Partial_Sums(s).(1+0)+s.2 by SERIES_1:def 1
.= Partial_Sums(s).0+s.1+s.2 by SERIES_1:def 1
.= s.0 + s.1 + s.2 by SERIES_1:def 1
.= 0 + s.1 + s.2 by A1
.= 1/((2-1)*(2+1)) by A1,A2
.= 3/4-1/(2*2)-1/(2*(2+1));
then
A9: X[2];
for n be Nat st n>=2 holds X[n] from NAT_1:sch 8(A9,A3);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n = 1/((2*n-1)*(2*n+1)) & s.0=0) implies for n
st n>=1 holds Partial_Sums(s).n = n/(2*n+1)
proof
defpred X[Nat] means Partial_Sums(s).$1= $1/(2*$1+1);
assume
A1: for n st n>=1 holds s.n = 1/((2*n-1)*(2*n+1)) & s.0=0;
A2: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A3: Partial_Sums(s).n = n/(2*n+1);
A4: n+1>=1 by NAT_1:11;
2*n+1>=1 by NAT_1:11;
then
A5: 2*n+1>0 by XXREAL_0:2;
2*n+3>=3 by NAT_1:11;
then
A6: 2*n+3>0 by XXREAL_0:2;
Partial_Sums(s).(n+1) =n/(2*n+1)+ s.(n+1) by A3,SERIES_1:def 1
.=n/(2*n+1)+1/((2*(n+1)-1)*(2*(n+1)+1)) by A1,A4
.=n/(2*n+1)+1/(2*n+1)*(1/(2*n+3)) by XCMPLX_1:102
.=n*(1/(2*n+1))+1/(2*n+1)*(1/(2*n+3)) by XCMPLX_1:99
.=(n+1/(2*n+3))*(1/(2*n+1))
.=((n*(2*n+3)+1)/(2*n+3))*(1/(2*n+1)) by A6,XCMPLX_1:113
.=((n+1)*(2*n+1))/(2*n+3)*(1/(2*n+1))
.=(2*n+1)*((n+1)/(2*n+3))*(1/(2*n+1)) by XCMPLX_1:74
.=(n+1)/(2*(n+1)+1) by A5,XCMPLX_1:107;
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.=0+s.1 by A1
.=1/((2*1-1)*(2*1+1)) by A1
.= 1/(2*1+1);
then
A7: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A7,A2);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n = 1/((3*n-2)*(3*n+1)) & s.0=0) implies for n
st n>=1 holds Partial_Sums(s).n = n/(3*n+1)
proof
defpred X[Nat] means Partial_Sums(s).$1= $1/(3*$1+1);
assume
A1: for n st n>=1 holds s.n = 1/((3*n-2)*(3*n+1)) & s.0=0;
A2: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A3: Partial_Sums(s).n = n/(3*n+1);
A4: n+1>=1 by NAT_1:11;
3*n+1>=1 by NAT_1:11;
then
A5: 3*n+1>0 by XXREAL_0:2;
3*n+4>=4 by NAT_1:11;
then
A6: 3*n+4>0 by XXREAL_0:2;
Partial_Sums(s).(n+1) =n/(3*n+1)+ s.(n+1) by A3,SERIES_1:def 1
.=n/(3*n+1)+1/((3*(n+1)-2)*(3*(n+1)+1)) by A1,A4
.=n/(3*n+1)+1/(3*n+1)*(1/(3*n+4)) by XCMPLX_1:102
.=n*(1/(3*n+1))+1/(3*n+1)*(1/(3*n+4)) by XCMPLX_1:99
.=(n+1/(3*n+4))*(1/(3*n+1))
.=((n*(3*n+4)+1)/(3*n+4))*(1/(3*n+1)) by A6,XCMPLX_1:113
.=((n+1)*(3*n+1))/(3*n+4)*(1/(3*n+1))
.=(3*n+1)*((n+1)/(3*n+4))*(1/(3*n+1)) by XCMPLX_1:74
.=(n+1)/(3*(n+1)+1) by A5,XCMPLX_1:107;
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.=0+s.1 by A1
.=1/((3*1-2)*(3*1+1)) by A1
.= 1/(3*1+1);
then
A7: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A7,A2);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n = 1/((2*n-1)*(2*n+1)*(2*n+3)) & s.0=0)
implies for n st n>=1 holds Partial_Sums(s).n =1/12-1/(4*(2*n+1)*(2*n+3))
proof
defpred X[Nat] means Partial_Sums(s).$1= 1/12-1/(4*(2*$1+1)*(2*$1+3));
assume
A1: for n st n>=1 holds s.n =1/((2*n-1)*(2*n+1)*(2*n+3)) & s.0=0;
A2: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A3: Partial_Sums(s).n =1/12-1/(4*(2*n+1)*(2*n+3));
A4: n+1>=1 by NAT_1:11;
2*n+1>=1 by NAT_1:11;
then
A5: 2*n+1>0 by XXREAL_0:2;
2*n+5>=5 by NAT_1:11;
then
A6: 2*n+5>0 by XXREAL_0:2;
Partial_Sums(s).(n+1)=1/12-1/(4*(2*n+1)*(2*n+3))+ s.(n+1) by A3,
SERIES_1:def 1
.=1/12-1/(4*(2*n+1)*(2*n+3))+1/((2*(n+1)-1)*(2*(n+1)+1)*(2*(n+1)+3))
by A1,A4
.=1/12-1/(4*((2*n+1)*(2*n+3)))+1/((2*n+1)*(2*n+3)*(2*n+5))
.=1/12-(1/4)*(1/((2*n+1)*(2*n+3)))+1/((2*n+1)*(2*n+3)*(2*n+5)) by
XCMPLX_1:102
.=1/12-(1/4)*(1/((2*n+1)*(2*n+3)))+(1/((2*n+1)*(2*n+3)))*(1/(2*n+5))
by XCMPLX_1:102
.=1/12-1/((2*n+1)*(2*n+3))*(1/4-1/(2*n+5))
.=1/12-1/((2*n+1)*(2*n+3))*((1*(2*n+5)-1*4)/(4*(2*n+5))) by A6,
XCMPLX_1:130
.=1/12-(1/(2*n+1))*(1/(2*n+3))*((2*n+1)/(4*(2*n+5))) by XCMPLX_1:102
.=1/12-(1/(2*n+1))*(1/(2*n+3))*(2*n+1)/(4*(2*n+5)) by XCMPLX_1:74
.=1/12-(1/(2*n+3))/(4*(2*n+5)) by A5,XCMPLX_1:109
.=1/12-1/((2*n+3)*(4*(2*n+5))) by XCMPLX_1:78
.=1/12-1/(4*(2*(n+1)+1)*(2*(n+1)+3));
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.=0+s.1 by A1
.=1/((2*1-1)*(2*1+1)*(2*1+3)) by A1
.= 1/12-1/(4*(2*1+1)*(2*1+3));
then
A7: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A7,A2);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n = 1/((3*n-2)*(3*n+1)*(3*n+4)) & s.0=0)
implies for n st n>=1 holds Partial_Sums(s).n =1/24-1/(6*(3*n+1)*(3*n+4))
proof
defpred X[Nat] means Partial_Sums(s).$1= 1/24-1/(6*(3*$1+1)*(3*$1+4));
assume
A1: for n st n>=1 holds s.n =1/((3*n-2)*(3*n+1)*(3*n+4)) & s.0=0;
A2: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A3: Partial_Sums(s).n =1/24-1/(6*(3*n+1)*(3*n+4));
A4: n+1>=1 by NAT_1:11;
3*n+1>=1 by NAT_1:11;
then
A5: 3*n+1>0 by XXREAL_0:2;
3*n+7>=7 by NAT_1:11;
then
A6: 3*n+7>0 by XXREAL_0:2;
Partial_Sums(s).(n+1)=1/24-1/(6*(3*n+1)*(3*n+4))+ s.(n+1) by A3,
SERIES_1:def 1
.=1/24-1/(6*(3*n+1)*(3*n+4))+1/((3*(n+1)-2)*(3*(n+1)+1)*(3*(n+1)+4))
by A1,A4
.=1/24-1/(6*((3*n+1)*(3*n+4)))+1/(((3*n+1)*(3*n+4))*(3*n+7))
.=1/24-(1/6)*(1/((3*n+1)*(3*n+4)))+1/(((3*n+1)*(3*n+4))*(3*n+7)) by
XCMPLX_1:102
.=1/24-(1/6)*(1/((3*n+1)*(3*n+4)))+(1/((3*n+1)*(3*n+4)))*(1/(3*n+7))
by XCMPLX_1:102
.=1/24-(1/((3*n+1)*(3*n+4)))*(1/6-1/(3*n+7))
.=1/24-(1/((3*n+1)*(3*n+4)))*((1*(3*n+7)-1*6)/(6*(3*n+7))) by A6,
XCMPLX_1:130
.=1/24-(1/(3*n+4))*(1/(3*n+1))*((3*n+1)/(6*(3*n+7))) by XCMPLX_1:102
.=1/24-(1/(3*n+4))*(1/(3*n+1))*(3*n+1)/(6*(3*n+7)) by XCMPLX_1:74
.=1/24-(1/(3*n+4))/(6*(3*n+7)) by A5,XCMPLX_1:109
.=1/24-1/((3*n+4)*(6*(3*n+7))) by XCMPLX_1:78
.=1/24-1/(6*(3*(n+1)+1)*(3*(n+1)+4));
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.=0+s.1 by A1
.=1/((3*1-2)*(3*1+1)*(3*1+4)) by A1
.=1/24-1/(6*(3*1+1)*(3*1+4));
then
A7: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A7,A2);
hence thesis;
end;
theorem
(for n holds s.n = (2*n-1)/(n*(n+1)*(n+2))) implies for n st n>=1
holds Partial_Sums(s).n = 3/4-2/(n+2)+1/(2*(n+1)*(n+2))
proof
defpred X[Nat] means Partial_Sums(s).$1= 3/4-2/($1+2)+1/(2*($1+1)*($1+2));
assume
A1: for n holds s.n = (2*n-1)/(n*(n+1)*(n+2));
then
A2: s.0 = (2*0-1)/(0*(0+1)*(0+2)) .= 0 by XCMPLX_1:49;
A3: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A4: Partial_Sums(s).n = 3/4-2/(n+2)+1/(2*(n+1)*(n+2));
n+1>=1+0 by NAT_1:11;
then
A5: n+1>0 by NAT_1:13;
n+2>=2 by NAT_1:11;
then n+2>0 by XXREAL_0:2;
then
A6: (n+1)*(n+2)>0 by A5,XREAL_1:129;
n+3>=3 by NAT_1:11;
then
A7: n+3>0 by XXREAL_0:2;
Partial_Sums(s).(n+1) = 3/4-2/(n+2)+1/(2*(n+1)*(n+2))+ s.(n+1) by A4,
SERIES_1:def 1
.= 3/4-2/(n+2)+1/(2*(n+1)*(n+2)) + (2*(n+1)-1)/((n+1)*((n+1)+1)*((n+1)
+2)) by A1
.= 3/4-(2/(n+2)-1/(2*((n+1)*(n+2))))+(2*n+1)/(((n+1)*(n+2))*(n+3))
.= 3/4-((2*(n+1))/((n+2)*(n+1))-1/(2*((n+1)*(n+2)))) +(2*n+1)/(((n+1)*
(n+2))*(n+3)) by A5,XCMPLX_1:91
.= 3/4-((2*(n+1)*2)/(2*(n+2)*(n+1))-1/(2*((n+1)*(n+2)))) +(2*n+1)/(((n
+1)*(n+2))*(n+3)) by XCMPLX_1:91
.= 3/4-((4*(n+1))-1)/(2*((n+2)*(n+1))) +(2*n+1)/(((n+1)*(n+2))*(n+3))
by XCMPLX_1:120
.= 3/4-((4*n+3)*(n+3))/(2*((n+2)*(n+1))*(n+3)) +(2*n+1)/(((n+1)*(n+2))
*(n+3)) by A7,XCMPLX_1:91
.= 3/4-((4*n+3)*(n+3))/(2*((n+2)*(n+1))*(n+3)) +((2*n+1)*2)/(((n+1)*(n
+2))*(n+3)*2) by XCMPLX_1:91
.= 3/4-(((4*n+3)*(n+3))/(2*((n+2)*(n+1))*(n+3)) -((2*n+1)*2)/(((n+1)*(
n+2))*(n+3)*2))
.= 3/4-((4*n+3)*(n+3)-((2*n+1)*2))/(2*((n+2)*(n+1))*(n+3))by XCMPLX_1:120
.= 3/4-(4*(n+1)*(n+2)-(n+1))/(2*((n+2)*(n+1))*(n+3))
.= 3/4-((4*((n+1)*(n+2)))/(2*(n+3)*((n+2)*(n+1))) -(n+1)/(2*((n+2)*(n+
1))*(n+3))) by XCMPLX_1:120
.= 3/4-(4/(2*(n+3))-1*(n+1)/(2*(n+2)*(n+3)*(n+1))) by A6,XCMPLX_1:91
.= 3/4-((2*2)/((n+3)*2)-1/(2*(n+2)*(n+3))) by A5,XCMPLX_1:91
.= 3/4-(2/((n+1+2))-1/(2*(n+1+1)*(n+1+2))) by XCMPLX_1:91;
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.=(2*1-1)/(1*(1+1)*(1+2)) by A1,A2
.= 3/4-2/(1+2)+1/(2*(1+1)*(1+2));
then
A8: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A8,A3);
hence thesis;
end;
theorem
(for n holds s.n = (n+2)/(n*(n+1)*(n+3))) implies for n st n>=1 holds
Partial_Sums(s).n = 29/36-1/(n+3)-3/(2*(n+2)*(n+3))-4/(3*(n+1)*(n+2)*(n+3))
proof
defpred X[Nat] means Partial_Sums(s).$1 = 29/36-1/($1+3)-3/(2*($1+2)*($1+3))
-4/(3*($1+1)*($1+2)*($1+3));
assume
A1: for n holds s.n = (n+2)/(n*(n+1)*(n+3));
then
A2: s.0 = (0+2)/(0*(0+1)*(0+3)) .= 0 by XCMPLX_1:49;
A3: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A4: Partial_Sums(s).n = 29/36-1/(n+3)-3/(2*(n+2)*(n+3))-4/(3*(n+1)*(n+
2) *(n+3));
n+4>=4 by NAT_1:11;
then
A5: n+4>0 by XXREAL_0:2;
n+1>=1+0 by NAT_1:11;
then
A6: n+1>0 by NAT_1:13;
then
A7: 2*(n+1)>0 by XREAL_1:129;
n+2>=2 by NAT_1:11;
then
A8: n+2>0 by XXREAL_0:2;
then
A9: (n+1)*(n+2)>0 by A6,XREAL_1:129;
then
A10: (n+1)*(n+2)*3>0 by XREAL_1:129;
n+3>=3 by NAT_1:11;
then
A11: n+3>0 by XXREAL_0:2;
then (n+1)*(n+2)*(n+3)>0 by A9,XREAL_1:129;
then
A12: (n+1)*(n+2)*(n+3)*6>0 by XREAL_1:129;
Partial_Sums(s).(n+1) =29/36-1/(n+3)-3/(2*(n+2)*(n+3))-4/(3*(n+1)*(n+
2)*(n+3))+s.(n+1) by A4,SERIES_1:def 1
.=29/36-1/(n+3)-3/(2*(n+2)*(n+3))-4/(3*(n+1)*(n+2)*(n+3))+(n+1+2)/((n+
1) *(n+1+1)*(n+1+3)) by A1
.=29/36-(1*(n+2))/((n+3)*(n+2))-3/(2*(n+2)*(n+3))-4/(3*(n+1)*(n+2) *(n
+3))+(n+3)/((n+1)*(n+2)*(n+4)) by A8,XCMPLX_1:91
.=29/36-((n+2)*2)/((n+2)*(n+3)*2)-3/(2*(n+2)*(n+3))-4/(3*(n+1)*(n+2) *
(n+3))+(n+3)/((n+1)*(n+2)*(n+4)) by XCMPLX_1:91
.=29/36-(((n+2)*2)/((n+2)*(n+3)*2)+3/(2*(n+2)*(n+3)))-4/(3*(n+1)*(n+2)
*(n+3))+(n+3)/((n+1)*(n+2)*(n+4))
.=29/36-(((n+2)*2)+3)/(2*(n+2)*(n+3))-4/(3*(n+1)*(n+2) *(n+3))+(n+3)/(
(n+1)*(n+2)*(n+4)) by XCMPLX_1:62
.=29/36-((n*2+7)*(n+1))/(2*(n+2)*(n+3)*(n+1))-4/(3*(n+1)*(n+2)*(n+3))
+(n+3)/((n+1)*(n+2)*(n+4)) by A6,XCMPLX_1:91
.=29/36-((n*2+7)*(n+1)*3)/(2*(n+2)*(n+3)*(n+1)*3)-4/(3*(n+1)*(n+2)*(n+
3)) +(n+3)/((n+1)*(n+2)*(n+4)) by XCMPLX_1:91
.=29/36-((n*2+7)*(n+1)*3)/(2*(n+2)*(n+3)*(n+1)*3)-(4*2)/(3*(n+1)*(n+2)
*(n+3) *2)+(n+3)/((n+1)*(n+2)*(n+4)) by XCMPLX_1:91
.=29/36-(((n*2+7)*(n+1)*3)/(6*(n+2)*(n+3)*(n+1))+8/(6*(n+1)*(n+2)*(n+3
))) +(n+3)/((n+1)*(n+2)*(n+4))
.=29/36-(((n*2+7)*(n+1)*3*(n+4))/(6*(n+2)*(n+3)*(n+1)*(n+4))+ 8/(6*(n+
1)*(n+2)*(n+3)))+(n+3)/((n+1)*(n+2)*(n+4)) by A5,XCMPLX_1:91
.=29/36-(((n*2+7)*(n+1)*3*(n+4))/(6*(n+1)*(n+2)*(n+3)*(n+4))+(8*(n+4))
/(6 *(n+1)*(n+2)*(n+3)*(n+4)))+(n+3)/((n+1)*(n+2)*(n+4))by A5,XCMPLX_1:91
.=29/36-((n*2+7)*(n+1)*3*(n+4)+8*(n+4))/(6*(n+1)*(n+2)*(n+3)*(n+4))+(n
+3) /((n+1)*(n+2)*(n+4)) by XCMPLX_1:62
.=29/36-((n*2+7)*(n+1)*3*(n+4)+8*(n+4))/(6*(n+1)*(n+2)*(n+3)*(n+4))+((
n+3) *6)/((n+1)*(n+2)*(n+4)*6) by XCMPLX_1:91
.=29/36-((n*2+7)*(n+1)*3*(n+4)+8*(n+4))/(6*(n+1)*(n+2)*(n+3)*(n+4))+((
n+3) *6*(n+3))/((n+1)*(n+2)*(n+4)*6*(n+3)) by A11,XCMPLX_1:91
.=29/36-(((n*2+7)*(n+1)*3*(n+4)+8*(n+4))/(6*(n+1)*(n+2)*(n+3)*(n+4)) -
((n+3)*6*(n+3))/((n+1)*(n+2)*(n+4)*6*(n+3)))
.=29/36-(((n*2+7)*(n+1)*3*(n+4)+8*(n+4))-((n+3)*6*(n+3))) /(6*(n+1)*(n
+2)*(n+3)*(n+4)) by XCMPLX_1:120
.=29/36-(6*(n+1)*(n+2)*(n+3)+9*(n+1)*(n+2)+8*(n+1)) /(6*(n+1)*(n+2)*(n
+3)*(n+4))
.=29/36-((6*(n+1)*(n+2)*(n+3)+9*(n+1)*(n+2))/(6*(n+1)*(n+2)*(n+3)*(n+4
)) +(8*(n+1))/(6*(n+1)*(n+2)*(n+3)*(n+4))) by XCMPLX_1:62
.=29/36-((1*(6*(n+1)*(n+2)*(n+3)))/((n+4)*(6*(n+1)*(n+2)*(n+3))) +(9*(
n+1)*(n+2))/(6*(n+1)*(n+2)*(n+3)*(n+4)) +(8*(n+1))/(6*(n+1)*(n+2)*(n+3)*(n+4)))
by XCMPLX_1:62
.=29/36-(1/(n+4)+(3*(3*(n+1)*(n+2)))/(2*(n+3)*(n+4)*(3*(n+1)*(n+2))) +
(8*(n+1))/(6*(n+1)*(n+2)*(n+3)*(n+4))) by A12,XCMPLX_1:91
.=29/36-(1/(n+4)+3/(2*(n+3)*(n+4)) +(4*(2*(n+1)))/(3*(n+2)*(n+3)*(n+4)
*(2*(n+1)))) by A10,XCMPLX_1:91
.=29/36-(1/(n+4)+3/(2*(n+3)*(n+4))+4/(3*(n+2)*(n+3)*(n+4))) by A7,
XCMPLX_1:91
.=29/36-1/(n+1+3)-3/(2*(n+1+2)*(n+1+3))-4/(3*(n+1+1)*(n+1+2)*(n+1+3));
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.=(1+2)/(1*(1+1)*(1+3)) by A1,A2
.=29/36-1/(1+3)-3/(2*(1+2)*(1+3))-4/(3*(1+1)*(1+2)*(1+3));
then
A13: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A13,A3);
hence thesis;
end;
theorem
(for n holds s.n = ((n+1)*2|^n)/((n+2)*(n+3))) implies for n holds
Partial_Sums(s).n = 2|^(n+1)/(n+3)-1/2
proof
defpred X[Nat] means Partial_Sums(s).$1 =2|^($1+1)/($1+3)-1/2;
assume
A1: for n holds s.n = ((n+1)*2|^n)/((n+2)*(n+3));
A2: for n st X[n] holds X[n+1]
proof
let n;
n+3>=3 by NAT_1:11;
then
A3: n+3>0 by XXREAL_0:2;
n+4>=4 by NAT_1:11;
then
A4: n+4>0 by XXREAL_0:2;
assume Partial_Sums(s).n = 2|^(n+1)/(n+3)-1/2;
then Partial_Sums(s).(n+1) = 2|^(n+1)/(n+3)-1/2 + s.(n+1) by SERIES_1:def 1
.= 2|^(n+1)/(n+3)-1/2 +((n+1+1)*2|^(n+1))/((n+1+2)*(n+1+3)) by A1
.= 2|^(n+1)/(n+3) +((n+2)*2|^(n+1))/((n+3)*(n+4))-1/2
.= (2|^(n+1)*(n+4))/((n+3)*(n+4)) +((n+2)*2|^(n+1))/((n+3)*(n+4))-1/2
by A4,XCMPLX_1:91
.= (2|^(n+1)*(n+4)+(n+2)*2|^(n+1))/((n+3)*(n+4))-1/2 by XCMPLX_1:62
.= (2|^(n+1)*2*(n+3))/((n+4)*(n+3))-1/2
.= (2|^(n+1)*2)/(n+4)-1/2 by A3,XCMPLX_1:91
.= 2|^(n+1+1)/(n+1+3)-1/2 by NEWTON:6;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=((0+1)*2|^0)/((0+2)*(0+3)) by A1
.=(1*1)/6 by NEWTON:4
.=2/3-1/2
.=2|^(0+1)/(0+3)-1/2;
then
A5: X[0];
for n holds X[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem
(for n holds s.n = (n|^2*4|^n)/((n+1)*(n+2))) implies for n st n>=1
holds Partial_Sums(s).n =2/3+((n-1)*4|^(n+1))/(3*(n+2))
proof
defpred X[Nat] means Partial_Sums(s).$1=2/3+(($1-1)*4|^($1+1))/(3*($1+2));
assume
A1: for n holds s.n = (n|^2*4|^n)/((n+1)*(n+2));
then
A2: s.0 = (0|^2*4|^0)/((0+1)*(0+2)) .= (0*4|^0)/(1*2) by NEWTON:11
.= 0;
A3: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A4: Partial_Sums(s).n =2/3+((n-1)*4|^(n+1))/(3*(n+2));
n+2>=2 by NAT_1:11;
then
A5: n+2>0 by XXREAL_0:2;
n+3>=3 by NAT_1:11;
then
A6: n+3>0 by XXREAL_0:2;
Partial_Sums(s).(n+1) =2/3+((n-1)*4|^(n+1))/(3*(n+2))+ s.(n+1) by A4,
SERIES_1:def 1
.=2/3+((n-1)*4|^(n+1))/(3*(n+2)) +((n+1)|^2*4|^(n+1))/(((n+1)+1)*((n+1
)+2)) by A1
.=2/3+((n-1)*4|^(n+1)*(n+3))/(3*(n+2)*(n+3)) +((n+1)|^2*4|^(n+1))/((n+
2)*(n+3)) by A6,XCMPLX_1:91
.=2/3+((n-1)*4|^(n+1)*(n+3))/(3*(n+2)*(n+3)) +((n+1)|^2*4|^(n+1)*3)/((
n+2)*(n+3)*3) by XCMPLX_1:91
.=2/3+(((n-1)*4|^(n+1)*(n+3))/(3*(n+2)*(n+3)) +((n+1)|^2*4|^(n+1)*3)/(
3*(n+2)*(n+3)))
.=2/3+(((n-1)*4|^(n+1)*(n+3))+((n+1)|^2*4|^(n+1)*3)) /(3*(n+2)*(n+3))
by XCMPLX_1:62
.=2/3+(((n-1)*(n+3)+(n+1)|^2*3)*4|^(n+1))/(3*(n+2)*(n+3))
.=2/3+(((n-1)*(n+3)+(n+1)*(n+1)*3)*4|^(n+1))/(3*(n+2)*(n+3)) by
WSIERP_1:1
.=2/3+(4*4|^(n+1)*n*(n+2))/(3*(n+3)*(n+2))
.=2/3+(4|^(n+1)*4*n)/(3*(n+3)) by A5,XCMPLX_1:91
.=2/3+((n+1-1)*4|^(n+1+1))/(3*(n+1+2)) by NEWTON:6;
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.=(1|^2*4|^1)/((1+1)*(1+2)) by A1,A2
.=(1*4|^1)/((1+1)*(1+2))
.=(1*4)/((1+1)*(1+2))
.=2/3+((1-1)*4|^(1+1))/(3*(1+2));
then
A7: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A7,A3);
hence thesis;
end;
theorem
(for n holds s.n = (n+2)/(n*(n+1)*2|^n)) implies for n st n>=1 holds
Partial_Sums(s).n =1-1/((n+1)*2|^n)
proof
defpred X[Nat] means Partial_Sums(s).$1=1-1/(($1+1)*2|^$1);
assume
A1: for n holds s.n = (n+2)/(n*(n+1)*2|^n);
then
A2: s.0 = (0+2)/(0*(0+1)*2|^0) .= 0 by XCMPLX_1:49;
A3: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A4: Partial_Sums(s).n =1-1/((n+1)*2|^n);
n+1>=1+0 by NAT_1:11;
then
A5: n+1>0 by NAT_1:13;
n+2>=2 by NAT_1:11;
then
A6: n+2>0 by XXREAL_0:2;
Partial_Sums(s).(n+1) =1-1/((n+1)*2|^n)+ s.(n+1) by A4,SERIES_1:def 1
.=1-1/((n+1)*2|^n)+((n+1)+2)/((n+1)*((n+1)+1)*2|^(n+1)) by A1
.=1-(1/((n+1)*2|^n)-(n+3)/((n+1)*(n+2)*2|^(n+1)))
.=1-(1*2/((n+1)*2|^n*2)-(n+3)/((n+1)*(n+2)*2|^(n+1))) by XCMPLX_1:91
.=1-(1*2/((n+1)*(2|^n*2))-(n+3)/((n+1)*(n+2)*2|^(n+1)))
.=1-(1*2/((n+1)*2|^(n+1))-(n+3)/((n+1)*(n+2)*2|^(n+1))) by NEWTON:6
.=1-(2*(n+2)/((n+1)*2|^(n+1)*(n+2))-(n+3)/((n+1)*(n+2)*2|^(n+1))) by A6,
XCMPLX_1:91
.=1-(2*(n+2)-(n+3))/((n+1)*(n+2)*2|^(n+1)) by XCMPLX_1:120
.=1-(1*(n+1))/((n+2)*2|^(n+1)*(n+1))
.=1-1/((n+1+1)*2|^(n+1)) by A5,XCMPLX_1:91;
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.=(1+2)/(1*(1+1)*2|^1) by A1,A2
.=(1+2)/(1*(1+1)*2)
.=1-1/((1+1)*2)
.=1-1/((1+1)*2|^1);
then
A7: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A7,A3);
hence thesis;
end;
theorem
(for n holds s.n = (2*n+3)/(n*(n+1)*3|^n)) implies for n st n>=1 holds
Partial_Sums(s).n = 1-1/((n+1)*3|^n)
proof
defpred X[Nat] means Partial_Sums(s).$1=1-1/(($1+1)*3|^$1);
assume
A1: for n holds s.n = (2*n+3)/(n*(n+1)*3|^n);
then
A2: s.0 = (2*0+3)/(0*(0+1)*3|^0) .= 0 by XCMPLX_1:49;
A3: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A4: Partial_Sums(s).n =1-1/((n+1)*3|^n);
n+1>=1+0 by NAT_1:11;
then
A5: n+1>0 by NAT_1:13;
n+2>=2 by NAT_1:11;
then
A6: n+2>0 by XXREAL_0:2;
Partial_Sums(s).(n+1) =1-1/((n+1)*3|^n)+ s.(n+1) by A4,SERIES_1:def 1
.=1-1/((n+1)*3|^n)+(2*(n+1)+3)/((n+1)*((n+1)+1)*3|^(n+1)) by A1
.=1-(1*3)/((n+1)*3|^n*3)+(2*n+5)/((n+1)*(n+2)*3|^(n+1)) by XCMPLX_1:91
.=1-3/((n+1)*(3|^n*3))+(2*n+5)/((n+1)*(n+2)*3|^(n+1))
.=1-3/((n+1)*3|^(n+1))+(2*n+5)/((n+1)*(n+2)*3|^(n+1)) by NEWTON:6
.=1-(3*(n+2))/((n+1)*3|^(n+1)*(n+2))+(2*n+5)/((n+1)*(n+2)*3|^(n+1)) by A6
,XCMPLX_1:91
.=1-((3*(n+2))/((n+1)*3|^(n+1)*(n+2))-(2*n+5)/((n+1)*(n+2)*3|^(n+1)))
.=1-(3*(n+2)-(2*n+5))/((n+1)*(n+2)*3|^(n+1)) by XCMPLX_1:120
.=1-(1*(n+1))/((n+2)*3|^(n+1)*(n+1))
.=1-1/((n+1+1)*3|^(n+1)) by A5,XCMPLX_1:91;
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.=(2*1+3)/(1*(1+1)*3|^1) by A1,A2
.=(2*1+3)/(1*(1+1)*3)
.=1-1/((1+1)*3)
.=1-1/((1+1)*3|^1);
then
A7: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A7,A3);
hence thesis;
end;
theorem
(for n holds s.n =((-1)|^n*2|^(n+1)) /((2|^(n+1)+(-1)|^(n+1))*(2|^(n+2
)+(-1)|^(n+2)))) implies for n holds Partial_Sums(s).n = 1/3+((-1)|^(n+2))/(3*(
2|^(n+2)+(-1)|^(n+2)))
proof
defpred X[Nat] means Partial_Sums(s).$1 = 1/3+((-1)|^($1+2))/(3*(
2|^($1+2)+(-1)|^($1+2)));
assume
A1: for n holds s.n =((-1)|^n*2|^(n+1)) /((2|^(n+1)+(-1)|^(n+1))*(2|^(n+
2)+(-1)|^(n+2)));
A2: for n st X[n] holds X[n+1]
proof
let n;
set b=2|^(n+2)+(-1)|^(n+2);
set p=2|^(n+3)+(-1)|^(n+3);
A3: b>0 by Lm18;
assume Partial_Sums(s).n =1/3+((-1)|^(n+2))/(3*(2|^(n+2)+(-1)|^(n+2)));
then
A4: Partial_Sums(s).(n+1) =1/3+((-1)|^(n+2))/(3*(2|^(n+2)+(-1)|^(n+2)))+s.
(n+1) by SERIES_1:def 1
.=1/3+((-1)|^(n+2))/(3*(2|^(n+2)+(-1)|^(n+2))) +((-1)|^(n+1)*2|^((n+1)
+1))/((2|^((n+1)+1)+(-1)|^((n+1)+1)) *(2|^((n+1)+2)+(-1)|^((n+1)+2))) by A1
.=1/3+((-1)|^(n+2))/(3*(2|^(n+2)+(-1)|^(n+2)))+((-1)|^(n+1)*2|^(n+2))
/((2|^(n+2)+(-1)|^(n+2))*(2|^(n+3)+(-1)|^(n+3)));
p>0 by Lm19;
then
Partial_Sums(s).(n+1) =1/3+((-1)|^(n+2)*p)/(3*b*p)+((-1)|^(n+1)*2|^(n+
2))/(b*p) by A4,XCMPLX_1:91
.=1/3+((-1)|^(n+2)*p)/(3*b*p)+((-1)|^(n+1)*2|^(n+2)*3)/(b*p*3) by
XCMPLX_1:91
.=1/3+(((-1)|^(n+2)*p)/(3*b*p)+((-1)|^(n+1)*2|^(n+2)*3)/(3*b*p))
.=1/3+(((-1)|^(n+2)*(-1)/(-1)*p)+((-1)|^(n+1)*2|^(n+2)*3))/(3*b*p) by
XCMPLX_1:62
.=1/3+(((-1)|^(n+2+1)/(-1)*p)+((-1)|^(n+1)*2|^(n+2)*3))/(3*b*p) by
NEWTON:6
.=1/3+(((-1)|^(n+3)/(-1)*p)+((-1)|^(n+1)*(-1)/(-1)*2|^(n+2)*3)) /(3*b*
p)
.=1/3+(((-1)|^(n+3)/(-1)*p)+((-1)|^(n+1+1)/(-1)*2|^(n+2)*3)) /(3*b*p)
by NEWTON:6
.=1/3+(((-1)|^(n+3)/(-1)*p)+((-1)|^(n+2)*(-1)/((-1)*(-1))*2|^(n+2)*3))
/(3*b*p)
.=1/3+(((-1)|^(n+3)/(-1)*p)+((-1)|^(n+2+1)/((-1)*(-1))*2|^(n+2)*3)) /(
3*b*p) by NEWTON:6
.=1/3+((-1)|^(n+3)*(2|^(n+2)+2|^(n+2)*2-2|^(n+3)-(-1)|^(n+3)))/(3*b*p)
.=1/3+((-1)|^(n+3)*(2|^(n+2)+2|^(n+2+1)-2|^(n+3)-(-1)|^(n+3)))/(3*b*p)
by NEWTON:6
.=1/3+((-1)|^(n+3)*(2|^(n+2)-(-1)|^(n+2)*(-1)))/(3*b*p) by NEWTON:6
.=1/3+((-1)|^(n+3)*b)/(3*p*b)
.=1/3+((-1)|^(n+2+1))/(3*(2|^(n+2+1)+(-1)|^(n+2+1))) by A3,XCMPLX_1:91;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=((-1)|^0*2|^(0+1)) /((2|^(0+1)+(-1)|^(0+1))*(2|^(0+2)+(-1)|^(0+2))) by A1
.=(1*2|^(0+1))/((2|^(0+1)+(-1)|^(0+1))*(2|^(0+2)+(-1)|^(0+2))) by NEWTON:4
.=(1*2)/((2|^(0+1)+(-1)|^(0+1))*(2|^(0+2)+(-1)|^(0+2)))
.=(1*2)/((2+(-1)|^(0+1))*(2|^(0+2)+(-1)|^(0+2)))
.=(1*2)/((2+(-1))*(2|^(0+2)+(-1)|^(0+2)))
.=(1*2)/((2+(-1))*(2*2+(-1)|^(0+2))) by WSIERP_1:1
.=(1*2)/((2+(-1))*(2*2+(-1)*(-1))) by WSIERP_1:1
.=1/3+((-1)*(-1))/(3*(2*2+(-1)*(-1)))
.=1/3+((-1)|^2)/(3*(2*2+(-1)*(-1))) by WSIERP_1:1
.=1/3+((-1)|^2)/(3*(2*2+(-1)|^2)) by WSIERP_1:1
.=1/3+((-1)|^(0+2))/(3*(2|^(0+2)+(-1)|^(0+2))) by WSIERP_1:1;
then
A5: X[0];
for n holds X[n] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem
(for n holds s.n = n!*n) implies for n st n>=1 holds Partial_Sums(s).n
= (n+1)!-1
proof
defpred X[Nat] means Partial_Sums(s).$1= ($1+1)!-1;
assume
A1: for n holds s.n = n!*n;
then
A2: s.0 = 0!*0 .= 0;
A3: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A4: Partial_Sums(s).n =(n+1)!-1;
Partial_Sums(s).(n+1)=(n+1)!-1+ s.(n+1) by A4,SERIES_1:def 1
.=(n+1)!-1 +(n+1)!*(n+1) by A1
.=(n+1)!*(n+1+1)-1
.=(n+1+1)!-1 by NEWTON:15;
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.= 1!*1 by A1,A2
.= (1+1)!-1 by NEWTON:13,14;
then
A5: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A5,A3);
hence thesis;
end;
theorem
(for n holds s.n = n/((n+1)!)) implies for n st n>=1 holds
Partial_Sums(s).n = 1-1/((n+1)!)
proof
defpred X[Nat] means Partial_Sums(s).$1= 1-1/(($1+1)!);
assume
A1: for n holds s.n = n/((n+1)!);
then
A2: s.0 = 0/((0+1)!) .= 0;
A3: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A4: Partial_Sums(s).n =1-1/((n+1)!);
n+2>=2 by NAT_1:11;
then
A5: n+2>0 by XXREAL_0:2;
Partial_Sums(s).(n+1)=1-1/((n+1)!)+ s.(n+1) by A4,SERIES_1:def 1
.=1-1/((n+1)!)+(n+1)/((n+1+1)!) by A1
.=1-(1*(n+2))/(((n+1)!)*(n+1+1))+(n+1)/((n+2)!) by A5,XCMPLX_1:91
.=1-(1*(n+2))/((n+1+1)!)+(n+1)/((n+2)!) by NEWTON:15
.=1-((n+2)/((n+1+1)!)-(n+1)/((n+2)!))
.=1-((n+2)-(n+1))/((n+2)!) by XCMPLX_1:120
.=1-1/((n+1+1)!);
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.= 1-1/((1+1)!) by A1,A2,NEWTON:14;
then
A6: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A6,A3);
hence thesis;
end;
theorem
(for n st n>=1 holds s.n = (n|^2+n-1)/((n+2)!) & s.0=0) implies for n
st n>=1 holds Partial_Sums(s).n = 1/2-(n+1)/((n+2)!)
proof
defpred X[Nat] means Partial_Sums(s).$1= 1/2-($1+1)/(($1+2)!);
assume
A1: for n st n>=1 holds s.n = (n|^2+n-1)/((n+2)!) & s.0=0;
A2: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A3: Partial_Sums(s).n =1/2-(n+1)/((n+2)!);
A4: n+1>=1 by NAT_1:11;
n+3>=3 by NAT_1:11;
then
A5: n+3>0 by XXREAL_0:2;
Partial_Sums(s).(n+1)=1/2-(n+1)/((n+2)!)+ s.(n+1) by A3,SERIES_1:def 1
.=1/2-(n+1)/((n+2)!)+((n+1)|^2+(n+1)-1)/((n+1+2)!) by A1,A4
.=1/2-((n+1)*(n+3))/((n+2)!*(n+2+1))+((n+1)|^2+n)/((n+3)!) by A5,
XCMPLX_1:91
.=1/2-((n+1)*(n+3))/((n+2+1)!)+((n+1)|^2+n)/((n+3)!) by NEWTON:15
.=1/2-(((n+1)*(n+3))/((n+3)!)-((n+1)|^2+n)/((n+3)!))
.=1/2-(((n+1)*(n+3))-((n+1)|^2+n))/((n+3)!) by XCMPLX_1:120
.=1/2-(((n+1)*(n+3))-(n+1)|^2-n)/((n+3)!)
.=1/2-((n+1)*(n+3)-(n+1)*(n+1)-n)/((n+3)!) by WSIERP_1:1
.=1/2-(n+1+1)/((n+1+2)!);
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.=0+s.1 by A1
.=(1|^2+1-1)/((1+2)!) by A1
.=(1*1)/((2+1)!)
.=1/(2*3) by NEWTON:14,15
.=1/2-2/(2!*(2+1)) by NEWTON:14
.=1/2-2/((2+1)!) by NEWTON:15;
then
A6: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A6,A2);
hence thesis;
end;
theorem
(for n holds s.n = (n*2|^n)/((n+2)!)) implies for n st n>=1 holds
Partial_Sums(s).n = 1-2|^(n+1)/((n+2)!)
proof
defpred X[Nat] means Partial_Sums(s).$1=1-2|^($1+1)/(($1+2)!);
assume
A1: for n holds s.n = (n*2|^n)/((n+2)!);
then
A2: s.0=(0*2|^0)/((0+2)!) .=0;
A3: for n be Nat st n>=1 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
n>=1 and
A4: Partial_Sums(s).n =1-2|^(n+1)/((n+2)!);
n+3>=3 by NAT_1:11;
then
A5: n+3>0 by XXREAL_0:2;
Partial_Sums(s).(n+1)=1-2|^(n+1)/((n+2)!)+ s.(n+1) by A4,
SERIES_1:def 1
.=1-2|^(n+1)/((n+2)!)+((n+1)*2|^(n+1))/((n+1+2)!) by A1
.=1-(2|^(n+1)*(n+3))/((n+2)!*(n+2+1))+((n+1)*2|^(n+1))/((n+3)!) by A5,
XCMPLX_1:91
.=1-(2|^(n+1)*(n+3))/((n+2+1)!)+((n+1)*2|^(n+1))/((n+3)!) by NEWTON:15
.=1-((2|^(n+1)*(n+3))/((n+2+1)!)-((n+1)*2|^(n+1))/((n+3)!))
.=1-(2|^(n+1)*(n+3)-2|^(n+1)*(n+1))/((n+3)!) by XCMPLX_1:120
.=1-(2|^(n+1)*2)/((n+3)!)
.=1-2|^(n+1+1)/((n+1+2)!) by NEWTON:6;
hence thesis;
end;
Partial_Sums(s).(1+0)=Partial_Sums(s).0+s.(1+0) by SERIES_1:def 1
.= s.0 + s.1 by SERIES_1:def 1
.=(1*2|^1)/((1+2)!) by A1,A2
.=2/((2+1)!)
.=2/(2*3) by NEWTON:14,15
.=1-(2*2)/(2!*(2+1)) by NEWTON:14
.=1-2|^2/(2!*(2+1)) by WSIERP_1:1
.=1-2|^(1+1)/((1+2)!) by NEWTON:15;
then
A6: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A6,A3);
hence thesis;
end;
:: Added by AG, 5.09.2005
theorem
(for n holds s.n = a*n+b) implies for n holds Partial_Sums(s).n = a*(n
+1)*n/2+n*b+b by Lm14;
::$N Sum of an arithmetic series
::$L https://en.wikipedia.org/wiki/Arithmetic_progression Sum of an arithmetic series
theorem
(for n holds s.n = a*n+b) implies
for n holds Partial_Sums(s).n = (n+1)*(s.0 + s.n)/2
proof
assume
A1: for n holds s.n = a*n+b;
let n;
Partial_Sums(s).n = a*(n+1)*n/2+n*b+b by A1,Lm14
.= (n+1)*(n*a+b+b)/2
.= (n+1)*(s.n+(a*0+b))/2 by A1
.= (n+1)*(s.n+s.0)/2 by A1;
hence thesis;
end;