:: Partial Sum and Partial Product of Some Series
:: by Jianbing Cao , Fahui Zhai and Xiquan Liang
::
:: Received November 7, 2005
:: Copyright (c) 2005-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, NEWTON, ARYTM_3, RELAT_1, ARYTM_1, CARD_1,
PREPOWER, XXREAL_0, FUNCT_1, SERIES_1, REALSET1, NAT_1, SERIES_3, REAL_1;
notations ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, SERIES_3,
SEQ_1, NEWTON, PREPOWER, SERIES_1;
constructors XXREAL_0, REAL_1, NAT_1, BINOP_2, NEWTON, PREPOWER, SERIES_1,
SERIES_3, VALUED_1, SUBSET_1;
registrations XCMPLX_0, XREAL_0, NAT_1, NEWTON, NUMBERS, VALUED_0, RELSET_1,
FUNCT_2, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, ARITHM;
theorems SERIES_3, NAT_1, PREPOWER, NEWTON, XCMPLX_1, SERIES_1, XREAL_1,
WSIERP_1;
schemes NAT_1;
begin
reserve n for Nat,
a,b,c,d for Real,
s for Real_Sequence;
Lm1: 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;
Lm2: ((1/2)|^(n+1)+2|^(n+1))|^2 = (1/4)|^(n+1)+4|^(n+1)+2
proof
((1/2)|^(n+1)+2|^(n+1))|^(1+1) =((1/2)|^(n+1)+2|^(n+1))|^1*((1/2)|^(n+1)
+2|^(n+1)) by NEWTON:6
.=((1/2)|^(n+1)+2|^(n+1))*((1/2)|^(n+1)+2|^(n+1))
.=((1/2)|^(n+1)*(1/2)|^(n+1)+(1/2)|^(n+1)*2|^(n+1)) +(2|^(n+1)*(1/2)|^(n
+1)+2|^(n+1)*2|^(n+1))
.=((1/2*(1/2))|^(n+1)+(1/2)|^(n+1)*2|^(n+1)) +(2|^(n+1)*(1/2)|^(n+1)+2|^
(n+1)*2|^(n+1)) by NEWTON:7
.=((1/2*1/2)|^(n+1)+(1/2*2)|^(n+1)) +(2|^(n+1)*(1/2)|^(n+1)+2|^(n+1)*2|^
(n+1)) by NEWTON:7
.=((1/2*1/2)|^(n+1)+(1/2*2)|^(n+1)) +((2*(1/2))|^(n+1)+2|^(n+1)*2|^(n+1)
) by NEWTON:7
.=((1/2*1/2)|^(n+1)+(1/2*2)|^(n+1)) +((2*(1/2))|^(n+1)+(2*2)|^(n+1)) by
NEWTON:7
.=((1/4)|^(n+1)+1)+(1|^(n+1)+4|^(n+1))
.=((1/4)|^(n+1)+1)+(1+4|^(n+1))
.=((1/4)|^(n+1)+2+4|^(n+1));
hence thesis;
end;
Lm3: ((1/3)|^(n+1)+3|^(n+1))|^2 = (1/9)|^(n+1)+9|^(n+1)+2
proof
((1/3)|^(n+1)+3|^(n+1))|^(1+1) =((1/3)|^(n+1)+3|^(n+1))|^1*((1/3)|^(n+1)
+3|^(n+1)) by NEWTON:6
.=((1/3)|^(n+1)+3|^(n+1))*((1/3)|^(n+1)+3|^(n+1))
.=((1/3)|^(n+1)*(1/3)|^(n+1)+(1/3)|^(n+1)*3|^(n+1)) +(3|^(n+1)*(1/3)|^(n
+1)+3|^(n+1)*3|^(n+1))
.=((1/3*(1/3))|^(n+1)+(1/3)|^(n+1)*3|^(n+1)) +(3|^(n+1)*(1/3)|^(n+1)+3|^
(n+1)*3|^(n+1)) by NEWTON:7
.=((1/3*1/3)|^(n+1)+(1/3*3)|^(n+1)) +(3|^(n+1)*(1/3)|^(n+1)+3|^(n+1)*3|^
(n+1)) by NEWTON:7
.=((1/3*1/3)|^(n+1)+(1/3*3)|^(n+1)) +((3*(1/3))|^(n+1)+3|^(n+1)*3|^(n+1)
) by NEWTON:7
.=((1/3*1/3)|^(n+1)+(1/3*3)|^(n+1)) +((3*(1/3))|^(n+1)+(3*3)|^(n+1)) by
NEWTON:7
.=((1/9)|^(n+1)+1)+(1|^(n+1)+9|^(n+1))
.=((1/9)|^(n+1)+1)+(1+9|^(n+1))
.=((1/9)|^(n+1)+2+9|^(n+1));
hence thesis;
end;
Lm4: (a-b)*(a+b) = a|^2-b|^2
proof
(a-b)*(a+b) = a*a -b*b .=a|^2-b*b by WSIERP_1:1
.= a|^2-b|^2 by WSIERP_1:1;
hence thesis;
end;
Lm5: (a-b)|^2=a|^2-2*a*b+b|^2
proof
(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;
hence thesis;
end;
Lm6: a <> 1 implies a*(1-a|^n)/(1-a)|^2-n*a|^(n+1)/(1-a)+n*a|^(n+1)+a|^(n+1) =
a*(1-a|^(n+1))/(1-a)|^2- (n+1)*a|^(n+2)/(1-a)
proof
assume a<>1;
then
A1: 1-a <> 0;
then
a*(1-a|^n)/(1-a)|^2-n*a|^(n+1)/(1-a)+n*a|^(n+1)+a|^(n+1) =a*(1-a|^n)/(1-
a)|^2-(1-a)*(n*a|^(n+1))/((1-a)*(1-a)) +n*a|^(n+1)+a|^(n+1) by XCMPLX_1:91
.=a*(1-a|^n)/(1-a)|^2-(1-a)*(n*a|^(n+1))/(1-a)|^2 +n*a|^(n+1)+a|^(n+1)
by WSIERP_1:1
.=((a-a*a|^n)-(n*a|^(n+1)-n*a|^(n+1)*a))/(1-a)|^2 +n*a|^(n+1)+a|^(n+1)
by XCMPLX_1:120
.=(a-a*a|^n-n*a|^(n+1)+a*n*a|^(n+1))/(1-a)|^2 +(n*a|^(n+1)+a|^(n+1))*1
.=(a-a*a|^n-n*a|^(n+1)+a*n*a|^(n+1))/(1-a)|^2 +(n*a|^(n+1)+a|^(n+1))*(((
1-a)/(1-a))*1) by A1,XCMPLX_1:60
.=(a-a*a|^n-n*a|^(n+1)+a*n*a|^(n+1))/(1-a)|^2 +(n*a|^(n+1)+a|^(n+1))*(((
1-a)/(1-a))*((1-a)/(1-a))) by A1,XCMPLX_1:60
.=(a-a*a|^n-n*a|^(n+1)+a*n*a|^(n+1))/(1-a)|^2 +(n*a|^(n+1)+a|^(n+1))*(((
1-a)*(1-a))/((1-a)*(1-a))) by XCMPLX_1:76
.=(a-a*a|^n-n*a|^(n+1)+a*n*a|^(n+1))/(1-a)|^2+(n*a|^(n+1) +a|^(n+1))*(((
1-a)|^1*(1-a))/((1-a)*(1-a)))
.=(a-a*a|^n-n*a|^(n+1)+a*n*a|^(n+1))/(1-a)|^2+(n*a|^(n+1) +a|^(n+1))*(((
1-a)|^(1+1))/((1-a)*(1-a))) by NEWTON:6
.=(a-a*a|^n-n*a|^(n+1)+a*n*a|^(n+1))/(1-a)|^2 +(n*a|^(n+1)+a|^(n+1))*((1
|^2-2*1*a+a|^2)/((1-a)*(1-a))) by Lm5
.=(a-a*a|^n-n*a|^(n+1)+a*n*a|^(n+1))/(1-a)|^2 +(n*a|^(n+1)+a|^(n+1))*((1
|^2-2*1*a+a|^2)/((1-a)|^2)) by WSIERP_1:1
.=(a-a*a|^n-n*a|^(n+1)+a*n*a|^(n+1))/(1-a)|^2 +(n*a|^(n+1)+a|^(n+1))*((1
-2*a+a|^2)/((1-a)|^2))
.=(a-a*a|^n-n*a|^(n+1)+a*n*a|^(n+1))/(1-a)|^2 +((n*a|^(n+1)+a|^(n+1))*(1
-2*a+a|^2))/((1-a)|^2) by XCMPLX_1:74
.=((a-a*a|^n-n*a|^(n+1)+a*n*a|^(n+1)) +((n*a|^(n+1)*1-n*a|^(n+1)*2*a+n*a
|^(n+1)*a|^2)+ (a|^(n+1)*1-a|^(n+1)*2*a+a|^(n+1)*a|^2)))/(1-a)|^2 by
XCMPLX_1:62
.=((a-a|^(n+1)-n*a|^(n+1)+a*n*a|^(n+1)) +((n*a|^(n+1)-n*a|^(n+1)*2*a+n*a
|^(n+1)*a|^2)+ (a|^(n+1)-a|^(n+1)*2*a+a|^(n+1)*a|^2)))/(1-a)|^2 by NEWTON:6
.=((a-a|^(n+1)*a)-(n+1)*a|^(n+1)*(a-a|^2))/(1-a)|^2
.=((a-a|^(n+1)*a)-(n+1)*a|^(n+1)*(a-a*a))/(1-a)|^2 by WSIERP_1:1
.=(a-a|^(n+1)*a)/(1-a)|^2 -(n+1)*a|^(n+1)*a*(1-a)/(1-a)|^2 by XCMPLX_1:120
.=(a-a|^(n+1)*a)/(1-a)|^2-((n+1)*a|^(n+1)*a)*(1-a)/((1-a)*(1-a)) by
WSIERP_1:1
.=(a-a|^(n+1)*a)/(1-a)|^2-(((n+1)*a|^(n+1)*a)/(1-a)*(1-a))/(1-a) by
XCMPLX_1:83
.=(a*(1-a|^(n+1)))/(1-a)|^2-((n+1)*(a|^(n+1)*a))/(1-a) by A1,XCMPLX_1:87
.=(a*(1-a|^(n+1)))/(1-a)|^2-((n+1)*a|^(n+1+1))/(1-a) by NEWTON:6
.=a*(1-a|^(n+1))/(1-a)|^2-(n+1)*a|^(n+2)/(1-a);
hence thesis;
end;
Lm7: 1/((2 -Root (n+2))+(2 -Root (n+1))) = (2 -Root (n+2))-(2 -Root (n+1))
proof
n+1+1 > n+1 by NAT_1:13;
then (2 -Root (n+2)) > (2 -Root (n+1)) by PREPOWER:28;
then (2 -Root (n+2))-(2 -Root (n+1)) > (2 -Root (n+1))-(2 -Root (n+1)) by
XREAL_1:9;
then
1/((2 -Root (n+2))+(2 -Root (n+1)))*1 =(1*((2 -Root (n+2))-(2 -Root (n+1
)))) /(((2 -Root (n+2))-(2 -Root (n+1)))*((2 -Root (n+2))+(2 -Root (n+1)))) by
XCMPLX_1:91
.=((2 -Root (n+2))-(2 -Root (n+1))) /((2 -Root (n+2))|^2-(2 -Root (n+1))
|^2) by Lm4
.=((2 -Root (n+2))-(2 -Root (n+1)))/((n+2)-(2 -Root (n+1))|^2) by
PREPOWER:19
.=((2 -Root (n+2))-(2 -Root (n+1)))/((n+2)-(n+1)) by PREPOWER:19
.=((2 -Root (n+2))-(2 -Root (n+1)));
hence thesis;
end;
theorem Th1:
(a+b+c)|^2=a|^2+b|^2+c|^2+2*a*b+2*a*c+2*b*c
proof
(a+b+c)|^(1+1) = (a+b+c)|^1*(a+b+c) by NEWTON:6
.= (a+b+c)*(a+b+c)
.= (a*a+a*b+a*c)+(a*b+b*b+b*c)+(a*c+c*b+c*c)
.= (a*a+a*b+a*c)+(a*b+b|^2+b*c)+(a*c+c*b+c*c) by WSIERP_1:1
.= (a|^2+a*b+a*c)+(a*b+b|^2+b*c)+(a*c+c*b+c*c) by WSIERP_1:1
.= (a|^2+a*b+a*c)+(a*b+b|^2+b*c)+(a*c+c*b+c|^2) by WSIERP_1:1
.= a|^2+c|^2+2*a*b+2*a*c+2*b*c+b|^2;
hence thesis;
end;
theorem Th2:
(a+b)|^3 = a|^3+3*a|^2*b+3*b|^2*a+b|^3
proof
(a+b)|^(2+1)=((a+b)|^2)*(a+b) by NEWTON:6
.=(a|^2+2*a*b+b|^2)*(a+b) by Lm1
.=a|^2*a+a|^2*b+(2*a*b*a+2*a*b*b)+(b|^2*a+b|^2*b)
.=a|^2*a+a|^2*b+(2*a*b*a+2*a*b*b)+(b|^2*a+b|^(2+1)) by NEWTON:6
.=a|^3+a|^2*b+(2*(a*a)*b+2*a*b*b)+(b|^2*a+b|^3) by NEWTON:6
.=a|^3+a|^2*b+(2*(a|^1*a)*b+2*a*b*b)+(b|^2*a+b|^3)
.=a|^3+a|^2*b+(2*(a|^(1+1))*b+2*a*b*b)+(b|^2*a+b|^3) by NEWTON:6
.=a|^3+3*a|^2*b+2*(b*b)*a+(b|^2*a+b|^3)
.=a|^3+3*a|^2*b+2*(b|^1*b)*a+(b|^2*a+b|^3)
.=a|^3+3*a|^2*b+2*(b|^(1+1))*a+(b|^2*a+b|^3) by NEWTON:6
.=a|^3+3*a|^2*b+3*b|^2*a+b|^3;
hence thesis;
end;
theorem
(a-b+c)|^2=a|^2+b|^2+c|^2-2*a*b+2*a*c-2*b*c
proof
(a-b+c)|^(1+1) = (a-b+c)|^1*(a-b+c) by NEWTON:6
.= (a-b+c)*(a-b+c)
.=(a*a-a*b+a*c)-(a*b-b*b+b*c)+(a*c-c*b+c*c)
.=(a*a-a*b+a*c)-(a*b-b|^2+b*c)+(a*c-c*b+c*c) by WSIERP_1:1
.=(a|^2-a*b+a*c)-(a*b-b|^2+b*c)+(a*c-c*b+c*c)by WSIERP_1:1
.=(a|^2-a*b+a*c)-(a*b-b|^2+b*c)+(a*c-c*b+c|^2) by WSIERP_1:1
.=a|^2+c|^2-2*a*b+2*a*c-2*b*c+b|^2;
hence thesis;
end;
theorem
(a-b-c)|^2=a|^2+b|^2+c|^2-2*a*b-2*a*c+2*b*c
proof
(a-b-c)|^(1+1) = (a-b-c)|^1*(a-b-c) by NEWTON:6
.= (a-b-c)*(a-b-c)
.=(a*a-a*b-a*c)-(a*b-b*b-b*c)-(a*c-c*b-c*c)
.=(a*a-a*b-a*c)-(a*b-b|^2-b*c)-(a*c-c*b-c*c) by WSIERP_1:1
.=(a|^2-a*b-a*c)-(a*b-b|^2-b*c)-(a*c-c*b-c*c)by WSIERP_1:1
.=(a|^2-a*b-a*c)-(a*b-b|^2-b*c)-(a*c-c*b-c|^2) by WSIERP_1:1
.=a|^2+c|^2-2*a*b-2*a*c+2*b*c+b|^2;
hence thesis;
end;
theorem
(a-b)|^3 = a|^3-3*a|^2*b+3*b|^2*a-b|^3
proof
(a-b)|^(2+1)=((a-b)|^2)*(a-b) by NEWTON:6
.=(a|^2-2*a*b+b|^2)*(a-b) by Lm5
.=a|^2*a-a|^2*b-(2*a*b*a-2*a*b*b)+(b|^2*a-b|^2*b)
.=a|^2*a-a|^2*b-(2*a*b*a-2*a*b*b)+(b|^2*a-b|^(2+1)) by NEWTON:6
.=a|^3-a|^2*b-(2*(a*a)*b-2*a*b*b)+(b|^2*a-b|^3) by NEWTON:6
.=a|^3-a|^2*b-(2*(a|^1*a)*b-2*a*b*b)+(b|^2*a-b|^3)
.=a|^3-a|^2*b-(2*(a|^(1+1))*b-2*a*b*b)+(b|^2*a-b|^3) by NEWTON:6
.=a|^3-3*a|^2*b+2*(b*b)*a+b|^2*a-b|^3
.=a|^3-3*a|^2*b+2*(b|^1*b)*a+b|^2*a-b|^3
.=a|^3-3*a|^2*b+2*b|^(1+1)*a+b|^2*a-b|^3 by NEWTON:6
.=a|^3-3*a|^2*b+3*b|^2*a-b|^3;
hence thesis;
end;
theorem
(a+b)|^4 = a|^4+4*a|^3*b+6*a|^2*b|^2+4*b|^3*a+b|^4
proof
(a+b)|^(3+1)=((a+b)|^3)*(a+b) by NEWTON:6
.=(a|^3+3*a|^2*b+3*b|^2*a+b|^3)*(a+b) by Th2
.=a|^3*a+a|^3*b+(3*a|^2*b*a+3*a|^2*b*b)+(3*b|^2*a*a+3*b|^2*a*b)+ (b|^3*a
+b|^3*b)
.=a|^3*a+a|^3*b+(3*a|^2*b*a+3*a|^2*b*b)+(3*b|^2*a*a+3*b|^2*a*b)+ (b|^3*a
+b|^(3+1)) by NEWTON:6
.=a|^4+a|^3*b+(3*(a|^2*a)*b+3*a|^2*b*b)+(3*b|^2*a*a+3*b|^2*a*b)+ (b|^3*a
+b|^4) by NEWTON:6
.=a|^4+a|^3*b+(3*(a|^(2+1))*b+3*a|^2*b*b)+(3*b|^2*a*a+3*b|^2*a*b)+ (b|^3
*a+b|^4) by NEWTON:6
.=a|^4+a|^3*b+(3*a|^3*b+3*a|^2*(b*b))+(3*b|^2*a*a+3*b|^2*a*b)+ (b|^3*a+b
|^4)
.=a|^4+a|^3*b+(3*a|^3*b+3*a|^2*(b|^1*b))+(3*b|^2*a*a+3*b|^2*a*b)+ (b|^3*
a+b|^4)
.=a|^4+a|^3*b+(3*a|^3*b+3*a|^2*(b|^(1+1)))+(3*b|^2*a*a+3*b|^2*a*b)+ (b|^
3*a+b|^4) by NEWTON:6
.=a|^4+a|^3*b+(3*a|^3*b+3*a|^2*b|^2)+(3*b|^2*(a*a)+3*b|^2*a*b)+ (b|^3*a+
b|^4)
.=a|^4+a|^3*b+(3*a|^3*b+3*a|^2*b|^2)+(3*b|^2*(a|^1*a)+3*b|^2*b*a)+ (b|^3
*a+b|^4)
.=a|^4+a|^3*b+(3*a|^3*b+3*a|^2*b|^2)+(3*b|^2*a|^(1+1)+3*(b|^2*b)*a)+ (b
|^3*a+b|^4) by NEWTON:6
.=a|^4+a|^3*b+(3*a|^3*b+3*a|^2*b|^2)+(3*b|^2*a|^2+3*(b|^(2+1))*a)+ (b|^3
*a+b|^4) by NEWTON:6
.=a|^4+4*a|^3*b+6*a|^2*b|^2+4*b|^3*a+b|^4;
hence thesis;
end;
theorem
(a+b+c+d)|^2 = a|^2+b|^2+c|^2+d|^2+(2*a*b+2*a*c+2*a*d) +(2*b*c+2*b*d)+ 2*c*d
proof
(a+b+c+d)|^(1+1) = (a+b+c+d)|^1*(a+b+c+d) by NEWTON:6
.=(a+b+c+d)*(a+b+c+d)
.=(a*a+a*b+a*c+a*d)+(a*b+b*b+b*c+b*d)+ (a*c+c*b+c*c+c*d)+(a*d+d*b+d*c+d*
d)
.=(a*a+a*b+a*c+a*d)+(a*b+b|^2+b*c+b*d)+ (a*c+c*b+c*c+c*d)+(a*d+d*b+d*c+d
*d) by WSIERP_1:1
.=(a|^2+a*b+a*c+a*d)+(a*b+b|^2+b*c+b*d)+ (a*c+c*b+c*c+c*d)+(a*d+d*b+d*c+
d*d) by WSIERP_1:1
.=(a|^2+a*b+a*c+a*d)+(a*b+b|^2+b*c+b*d)+ (a*c+c*b+c|^2+c*d)+(a*d+d*b+d*c
+d*d) by WSIERP_1:1
.=(a|^2+a*b+a*c+a*d)+(a*b+b|^2+b*c+b*d)+ (a*c+c*b+c|^2+c*d)+(a*d+d*b+d*c
+d|^2) by WSIERP_1:1
.=a|^2+c|^2+b|^2+d|^2+(2*a*b+2*a*c+2*a*d)+(2*b*c+2*b*d)+2*c*d;
hence thesis;
end;
theorem
(a+b+c)|^3=a|^3+b|^3+c|^3+(3*a|^2*b+3*a|^2*c)+ (3*b|^2*a+3*b|^2*c)+(3*
c|^2*a+3*c|^2*b)+6*a*b*c
proof
(a+b+c)|^(2+1)=((a+b+c)|^2)*(a+b+c) by NEWTON:6
.=(a|^2+b|^2+c|^2+2*a*b+2*a*c+2*b*c)*(a+b+c) by Th1
.=(a|^2*a+a|^2*b+a|^2*c)+(b|^2*a+b|^2*b+b|^2*c) +(c|^2*a+c|^2*b+c|^2*c)+
(2*a*b*a+2*a*b*b+2*a*b*c) +(2*a*c*a+2*a*c*b+2*a*c*c)+(2*b*c*a+2*b*c*b+2*b*c*c)
.=(a|^(2+1)+a|^2*b+a|^2*c)+(b|^2*a+b|^2*b+b|^2*c) +(c|^2*a+c|^2*b+c|^2*c
)+(2*a*b*a+2*a*b*b+2*a*b*c) +(2*a*c*a+2*a*c*b+2*a*c*c)+(2*b*c*a+2*b*c*b+2*b*c*c
) by NEWTON:6
.=(a|^3+a|^2*b+a|^2*c)+(b|^2*a+b|^(2+1)+b|^2*c) +(c|^2*a+c|^2*b+c|^2*c)+
(2*a*b*a+2*a*b*b+2*a*b*c) +(2*a*c*a+2*a*c*b+2*a*c*c)+(2*b*c*a+2*b*c*b+2*b*c*c)
by NEWTON:6
.=(a|^3+a|^2*b+a|^2*c)+(b|^2*a+b|^3+b|^2*c)+(c|^2*a+c|^2*b+c|^3)+ (2*(a*
a)*b+2*a*(b*b)+2*a*b*c)+(2*(a*a)*c+2*a*c*b+2*a*(c*c)) +(2*b*c*a+2*(b*b)*c+2*b*(
c*c)) by NEWTON:6
.=(a|^3+a|^2*b+a|^2*c)+(b|^2*a+b|^3+b|^2*c)+(c|^2*a+c|^2*b+c|^3)+ (2*(a
|^1*a)*b+2*a*(b*b)+2*a*b*c)+(2*(a*a)*c+2*a*c*b+2*a*(c*c)) +(2*b*c*a+2*(b*b)*c+2
*b*(c*c))
.=(a|^3+a|^2*b+a|^2*c)+(b|^2*a+b|^3+b|^2*c)+(c|^2*a+c|^2*b+c|^3)+ (2*(a
|^(1+1))*b+2*a*(b*b)+2*a*b*c)+(2*(a*a)*c+2*a*c*b+2*a*(c*c)) +(2*b*c*a+2*(b*b)*c
+2*b*(c*c)) by NEWTON:6
.=(a|^3+a|^2*b+a|^2*c)+(b|^2*a+b|^3+b|^2*c)+(c|^2*a+c|^2*b+c|^3)+ (2*a|^
2*b+2*a*(b|^1*b)+2*a*b*c)+(2*(a*a)*c+2*a*c*b+2*a*(c*c)) +(2*b*c*a+2*(b*b)*c+2*b
*(c*c))
.=(a|^3+a|^2*b+a|^2*c)+(b|^2*a+b|^3+b|^2*c)+(c|^2*a+c|^2*b+c|^3)+ (2*a|^
2*b+2*a*b|^(1+1)+2*a*b*c)+(2*(a*a)*c+2*a*c*b+2*a*(c*c)) +(2*b*c*a+2*(b*b)*c+2*b
*(c*c)) by NEWTON:6
.=(a|^3+a|^2*b+a|^2*c)+(b|^2*a+b|^3+b|^2*c)+(c|^2*a+c|^2*b+c|^3)+ (2*a|^
2*b+2*a*b|^2+2*a*b*c)+(2*(a|^2)*c+2*a*c*b+2*a*(c*c)) +(2*b*c*a+2*(b*b)*c+2*b*(c
*c)) by WSIERP_1:1
.=(a|^3+a|^2*b+a|^2*c)+(b|^2*a+b|^3+b|^2*c)+(c|^2*a+c|^2*b+c|^3)+ (2*a|^
2*b+2*a*b|^2+2*a*b*c)+(2*a|^2*c+2*a*c*b+2*a*(c|^2)) +(2*b*c*a+2*(b*b)*c+2*b*(c*
c)) by WSIERP_1:1
.=(a|^3+a|^2*b+a|^2*c)+(b|^2*a+b|^3+b|^2*c)+(c|^2*a+c|^2*b+c|^3)+ (2*a|^
2*b+2*a*b|^2+2*a*b*c)+(2*a|^2*c+2*a*c*b+2*a*(c|^2)) +(2*b*c*a+2*(b*b)*c+2*b*(c
|^2)) by WSIERP_1:1
.=(a|^3+b|^3+c|^3+a|^2*b+a|^2*c)+(b|^2*a+b|^2*c)+(c|^2*a+c|^2*b)+ (2*a|^
2*b+2*a*b|^2+2*a*b*c)+(2*a|^2*c+2*a*c*b+2*a*c|^2) +(2*b*c*a+2*b|^2*c+2*(c|^2)*b
) by WSIERP_1:1
.=(a|^3+b|^3+c|^3)+(3*a|^2*b+3*a|^2*c)+ (3*b|^2*a+3*b|^2*c)+(3*c|^2*a+3*
c|^2*b)+6*a*b*c;
hence thesis;
end;
theorem
a<>0 implies ((1/a)|^(n+1)+a|^(n+1))|^2 = (1/a)|^(2*n+2)+a|^(2*n+2)+2
proof
assume
A1: a<>0;
((1/a)|^(n+1)+a|^(n+1))|^(1+1) =((1/a)|^(n+1)+a|^(n+1))|^1*((1/a)|^(n+1)
+a|^(n+1)) by NEWTON:6
.=((1/a)|^(n+1)+a|^(n+1))*((1/a)|^(n+1)+a|^(n+1))
.=((1/a)|^(n+1)*(1/a)|^(n+1)+(1/a)|^(n+1)*a|^(n+1)) +(a|^(n+1)*(1/a)|^(n
+1)+a|^(n+1)*a|^(n+1))
.=((1/a*(1/a))|^(n+1)+(1/a)|^(n+1)*a|^(n+1)) +(a|^(n+1)*(1/a)|^(n+1)+a|^
(n+1)*a|^(n+1)) by NEWTON:7
.=((1/a*(1/a))|^(n+1)+(1/a*a)|^(n+1)) +(a|^(n+1)*(1/a)|^(n+1)+a|^(n+1)*a
|^(n+1)) by NEWTON:7
.=((1/a*(1/a))|^(n+1)+(1/a*a)|^(n+1)) +((a*(1/a))|^(n+1)+a|^(n+1)*a|^(n+
1)) by NEWTON:7
.=((1/a*(1/a))|^(n+1)+(1/a*a)|^(n+1)) +((a*(1/a))|^(n+1)+(a*a)|^(n+1))
by NEWTON:7
.=((1/a*(1/a))|^(n+1)+1|^(n+1))+((1/a*a)|^(n+1)+(a*a)|^(n+1)) by A1,
XCMPLX_1:106
.=((1/a*(1/a))|^(n+1)+1|^(n+1))+(1|^(n+1)+(a*a)|^(n+1)) by A1,XCMPLX_1:106
.=((1/a*(1/a))|^(n+1)+1)+(1|^(n+1)+(a*a)|^(n+1))
.=((1/a*(1/a))|^(n+1)+1)+(1+(a*a)|^(n+1))
.=(((1/a)*(1/a))|^(n+1)+(a*a)|^(n+1))+2
.=((1/a)*(1/a))|^(n+1)+(a|^2)|^(n+1)+2 by WSIERP_1:1
.=((1/a)*(1/a))|^(n+1)+a|^(2*(n+1))+2 by NEWTON:9
.=((1/a)|^2)|^(n+1)+a|^(2*n+2)+2 by WSIERP_1:1
.=(1/a)|^(2*(n+1))+a|^(2*n+2)+2 by NEWTON:9
.=(1/a)|^(2*n+2)+a|^(2*n+2)+2;
hence thesis;
end;
:: Geometrical Series
theorem
(a <> 1 & for n holds s.n = a|^n) implies Partial_Sums(s).n = (1 - a|^
(n+1))/(1-a)
proof
defpred X[Nat] means Partial_Sums(s).$1 = (1 - a|^($1+1))/(1-a);
assume a<>1;
then
A1: 1-a <> 0;
assume
A2: for n holds s.n = a|^n;
A3: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = (1 - a|^(n+1))/(1-a);
hence Partial_Sums(s).(n+1) = (1 - a|^(n+1))/(1-a) + s.(n+1) by
SERIES_1:def 1
.= (1 - a |^(n+1))/(1-a) + a|^(n+1) * 1 by A2
.= (1-a|^(n+1))/(1-a)+a|^(n+1)*((1-a)/(1-a)) by A1,XCMPLX_1:60
.= (1-a|^(n+1))/(1-a)+(a|^(n+1)*(1-a))/(1-a) by XCMPLX_1:74
.= (1-a|^(n+1) + (a|^(n+1)-a |^ (n+1)*a))/(1-a) by XCMPLX_1:62
.= (1-a|^(n+1) + (a|^(n+1)-a|^(n+1+1)))/(1-a) by NEWTON:6
.= (1 - a|^(n+1+1))/(1-a);
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.= a|^0 by A2
.= 1 by NEWTON:4
.= (1-a)/(1-a) by A1,XCMPLX_1:60
.= (1-a|^(0+1))/(1-a);
then
A4: X[0];
for n holds X[n] from NAT_1:sch 2(A4,A3);
hence thesis;
end;
theorem
(a <> 1 & a <> 0 & for n holds s.n = (1/a)|^n) implies for n holds
Partial_Sums(s).n = ((1/a)|^n-a)/(1-a)
proof
assume that
A1: a<>1 and
A2: a <> 0;
defpred X[Nat] means Partial_Sums(s).$1 = ((1/a)|^$1-a)/(1-a);
assume
A3: for n holds s.n = (1/a)|^n;
A4: 1-a <> 0 by A1;
A5: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = ((1/a)|^n-a)/(1-a);
hence Partial_Sums(s).(n+1) = ((1/a)|^n-a)/(1-a)+ s.(n+1) by SERIES_1:def 1
.= ((1/a)|^n-a)/(1-a) + (1/a)|^(n+1) * 1 by A3
.= ((1/a)|^n-a)/(1-a)+(1/a)|^(n+1)*((1-a)/(1-a)) by A4,XCMPLX_1:60
.= ((1/a)|^n-a)/(1-a)+((1/a)|^(n+1)*(1-a))/(1-a) by XCMPLX_1:74
.= ((1/a)|^n-a + ((1/a)|^(n+1)*1-(1/a)|^(n+1)*a))/(1-a) by XCMPLX_1:62
.= ((1/a)|^n-a + (1/a)|^(n+1)-((1/a)|^(n+1))*a)/(1-a)
.= ((1/a)|^n-a + (1/a)|^(n+1)-((1/a)|^n*(1/a))*a)/(1-a) by NEWTON:6
.= ((1/a)|^n-a + (1/a)|^(n+1)-(1/a)|^n*(1/a*a))/(1-a)
.= ((1/a)|^n-a + (1/a)|^(n+1)-(1/a)|^n*1)/(1-a) by A2,XCMPLX_1:106
.= ((1/a)|^(n+1)-a)/(1-a);
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.= (1/a)|^0 by A3
.= 1 by NEWTON:4
.= (1-a)/(1-a) by A4,XCMPLX_1:60
.= ((1/a)|^0-a)/(1-a) by NEWTON:4;
then
A6: X[0];
for n holds X[n] from NAT_1:sch 2(A6,A5);
hence thesis;
end;
:: Compositive Series
theorem
(for n holds s.n = 10|^n+2*n+1) implies Partial_Sums(s).n = 10|^(n+1)/
9-1/9+(n+1)|^2
proof
defpred X[Nat] means Partial_Sums(s).$1 =10|^($1+1)/9-1/9+($1+1)|^2;
assume
A1: for n holds s.n = 10|^n+2*n+1;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = 10|^(n+1)/9-1/9+(n+1)|^2;
then Partial_Sums(s).(n+1) = 10|^(n+1)/9-1/9+(n+1)|^2 + s.(n+1) by
SERIES_1:def 1
.= 10|^(n+1)/9-1/9+(n+1)|^2+(10|^(n+1)+2*(n+1)+1) by A1
.= (10|^(n+1)*10)/9-1/9+((n+1)|^2+2*n+3)
.= (10|^(n+1)*10)/9-1/9+(n|^2+2*n*1+1|^2+2*n+3) by Lm1
.= (10|^(n+1)*10)/9-1/9+(n|^2+2*n+1+2*n+3)
.= ((10|^(n+1)*10)/9-1/9)+(n|^2+2*n*2+2|^2) by Lm1
.= ((10|^(n+1)*10)/9-1/9)+(n+2)|^2 by Lm1
.= 10|^(n+1+1)/9-1/9+(n+2)|^2 by NEWTON:6;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=10|^0+2*0+1 by A1
.=10/9-1/9+1 by NEWTON:4
.=10|^(0+1)/9-1/9+1
.=10|^(0+1)/9-1/9+(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 = 2*n-1+(1/2)|^n) implies Partial_Sums(s).n =n|^2+1-(
1/2)|^n
proof
defpred X[Nat] means Partial_Sums(s).$1 =$1|^2+1-(1/2)|^$1;
assume
A1: for n holds s.n = 2*n-1+(1/2)|^n;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = n|^2+1-(1/2)|^n;
then Partial_Sums(s).(n+1) =n|^2+1-(1/2)|^n+ s.(n+1) by SERIES_1:def 1
.=n|^2+1-(1/2)|^n+(2*(n+1)-1+(1/2)|^(n+1)) by A1
.=n|^2+1-(1/2)|^n+(1/2)|^(n+1)+2*(n+1)-1
.=n|^2+1-(1/2)|^n+(1/2)|^n*(1/2)+2*(n+1)-1 by NEWTON:6
.=n|^2+1-((1/2)|^n*(1/2))+2*(n+1)-1
.=n|^2+1-(1/2)|^(n+1)+2*(n+1)-1 by NEWTON:6
.=(n|^2+2*n+1)+1-(1/2)|^(n+1)
.=(n|^2+2*n*1+1|^2)+1-(1/2)|^(n+1)
.=(n+1)|^2+1-(1/2)|^(n+1) by Lm1;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=2*0-1+(1/2)|^0 by A1
.=-1+1 by NEWTON:4
.=1-1+0|^2 by NEWTON:11
.=1-(1/2)|^0+0|^2 by NEWTON:4;
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*(1/2)|^n) implies Partial_Sums(s).n =2-(2+n)*(1/2 )|^n
proof
defpred X[Nat] means Partial_Sums(s).$1 =2-(2+$1)*(1/2)|^$1;
assume
A1: for n holds s.n = n*(1/2)|^n;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = 2-(2+n)*(1/2)|^n;
then Partial_Sums(s).(n+1) =2-(2+n)*(1/2)|^n+s.(n+1) by SERIES_1:def 1
.=2-(2+n)*(1/2)|^n+(n+1)*(1/2)|^(n+1) by A1
.=2-2*(1/2)|^n-n*(1/2)|^n+n*((1/2)|^(n+1))+1*(1/2)|^(n+1)
.=2-((4*1/2)*(1/2)|^n)-n*(1/2)|^n+n*((1/2)|^n*(1/2))+1*(1/2)|^(n+1) by
NEWTON:6
.=2-4*((1/2)|^n*(1/2))-n*(1/2)|^n+n*(1/2)|^n*(1/2)+1*(1/2)|^(n+1)
.=2-4*((1/2)|^(n+1))-n*(1/2)|^n+n*(1/2)|^n*(1/2)+1*(1/2)|^(n+1) by
NEWTON:6
.=2-3*(1/2)|^(n+1)-n*((1/2)|^n*(1/2))
.=2-3*(1/2)|^(n+1)-n*(1/2)|^(n+1) by NEWTON:6
.=2-(3+n)*(1/2)|^(n+1);
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0*(1/2)|^0 by A1
.=2-(2+0)*1
.=2-(2+0)*(1/2)|^0 by NEWTON:4;
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/2)|^n+2|^n)|^2) implies for n holds
Partial_Sums(s).n=-(1/4)|^n/3+4|^(n+1)/3+2*n+3
proof
defpred X[Nat] means Partial_Sums(s).$1 =-(1/4)|^$1/3+4|^($1+1)/3+2*$1+3;
assume
A1: for n holds s.n = ((1/2)|^n+2|^n)|^2;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = -(1/4)|^n/3+4|^(n+1)/3+2*n+3;
then Partial_Sums(s).(n+1) =-(1/4)|^n/3+4|^(n+1)/3+2*n+3+s.(n+1) by
SERIES_1:def 1
.=-(1/4)|^n/3+4|^(n+1)/3+2*n+3+(((1/2)|^(n+1)+2|^(n+1))|^2) by A1
.=-(1/4)|^n/3+4|^(n+1)/3+2*n+3+((1/4)|^(n+1)+4|^(n+1)+2) by Lm2
.=-(1/4)|^n/3+(1/4)|^(n+1)+4|^(n+1)/3+4|^(n+1)+2*(n+1)+3
.=-(1/4)|^n/3+(1/4)|^n*(1/4)+4|^(n+1)/3+4|^(n+1)+2*(n+1)+3 by NEWTON:6
.=-((1/4)|^n*(1/4))/3+4|^(n+1)/3+4|^(n+1)+2*(n+1)+3
.=-(1/4)|^(n+1)/3+4|^(n+1)/3+4|^(n+1)+2*(n+1)+3 by NEWTON:6
.=-(1/4)|^(n+1)/3+(4|^(n+1)*4)/3+2*(n+1)+3
.=-(1/4)|^(n+1)/3+4|^(n+1+1)/3+2*(n+1)+3 by NEWTON:6;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=((1/2)|^0+2|^0)|^2 by A1
.=(1+2|^0)|^2 by NEWTON:4
.=(1+1)|^2 by NEWTON:4
.=-1/3+4/3+2*0+3 by Lm1
.=-(1/4)|^0/3+4/3+2*0+3 by NEWTON:4
.=-(1/4)|^0/3+4|^(0+1)/3+2*0+3;
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/3)|^n+3|^n)|^2) implies for n holds
Partial_Sums(s).n = -(1/9)|^n/8+9|^(n+1)/8+2*n+3
proof
defpred X[Nat] means Partial_Sums(s).$1 =-(1/9)|^$1/8+9|^($1 +1)/8+2*$1+3;
assume
A1: for n holds s.n = ((1/3)|^n+3|^n)|^2;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n =-(1/9)|^n/8+9|^(n+1)/8+2*n+3;
then Partial_Sums(s).(n+1) =-(1/9)|^n/8+9|^(n+1)/8+2*n+3+s.(n+1) by
SERIES_1:def 1
.=-(1/9)|^n/8+9|^(n+1)/8+2*n+3+(((1/3)|^(n+1)+3|^(n+1))|^2) by A1
.=-(1/9)|^n/8+9|^(n+1)/8+2*n+3+((1/9)|^(n+1)+9|^(n+1)+2) by Lm3
.=-(1/9)|^n/8+(1/9)|^(n+1)+9|^(n+1)/8+9|^(n+1)+2*(n+1)+3
.=-(1/9)|^n/8+(1/9)|^n*(1/9)+9|^(n+1)/8+9|^(n+1)+2*(n+1)+3 by NEWTON:6
.=-((1/9)|^n*(1/9))/8+9|^(n+1)/8+9|^(n+1)+2*(n+1)+3
.=-(1/9)|^(n+1)/8+9|^(n+1)/8+9|^(n+1)+2*(n+1)+3 by NEWTON:6
.=-(1/9)|^(n+1)/8+(9|^(n+1)*9)/8+2*(n+1)+3
.=-(1/9)|^(n+1)/8+9|^(n+1+1)/8+2*(n+1)+3 by NEWTON:6;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=((1/3)|^0+3|^0)|^2 by A1
.=(1+3|^0)|^2 by NEWTON:4
.=(1+1)|^2 by NEWTON:4
.=-1/8+9/8+2*0+3 by Lm1
.=-(1/9)|^0/8+9/8+2*0+3 by NEWTON:4
.=-(1/9)|^0/8+9|^(0+1)/8+2*0+3;
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|^n) implies for n holds Partial_Sums(s).n = n*2
|^(n+1)-2|^(n+1)+2
proof
defpred X[Nat] means Partial_Sums(s).$1 =$1*2|^($1+1)-2|^($1+1)+2;
assume
A1: for n holds s.n = n*2|^n;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = n*2|^(n+1)-2|^(n+1)+2;
then Partial_Sums(s).(n+1) =n*2|^(n+1)-2|^(n+1)+2+s.(n+1) by SERIES_1:def 1
.=n*2|^(n+1)-2|^(n+1)+2+(n+1)*2|^(n+1) by A1
.=n*(2|^(n+1)*2)+2
.=n*2|^(n+1+1)+2 by NEWTON:6;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0*2|^0 by A1
.=0*2|^(0+1)-2+2
.=0*2|^(0+1)-2|^(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 = (2*n+1)*3|^n) implies for n holds Partial_Sums(s).n
= n*3|^(n+1)+1
proof
defpred X[Nat] means Partial_Sums(s).$1 =$1*3|^($1+1)+1;
assume
A1: for n holds s.n = (2*n+1)*3|^n;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = n*3|^(n+1)+1;
then Partial_Sums(s).(n+1) = n*3|^(n+1)+1+s.(n+1) by SERIES_1:def 1
.=n*3|^(n+1)+1+(2*(n+1)+1)*3|^(n+1) by A1
.=(n+1)*(3|^(n+1)*3)+1
.=(n+1)*3|^(n+1+1)+1 by NEWTON:6;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=(2*0+1)*3|^0 by A1
.=0*3|^(0+1)+1 by NEWTON:4;
then
A3: X[0];
for n holds X[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
(a <> 1 & for n holds s.n = n*a|^n) implies for n holds Partial_Sums(s
).n = a*(1-a|^n)/(1-a)|^2 - n*a|^(n+1)/(1-a)
proof
assume that
A1: a <> 1 and
A2: for n holds s.n = n*a|^n;
defpred X[Nat] means Partial_Sums(s).$1 =a*(1-a|^$1)/(1-a)|^2-$1*
a|^($1+1)/(1-a);
A3: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = a*(1-a|^n)/(1-a)|^2-n*a|^(n+1)/(1-a);
then
Partial_Sums(s).(n+1) =a*(1-a|^n)/(1-a)|^2-n*a|^(n+1)/(1-a)+s.(n+1) by
SERIES_1:def 1
.=a*(1-a|^n)/(1-a)|^2-n*a|^(n+1)/(1-a)+(n+1)*a|^(n+1) by A2
.=a*(1-a|^n)/(1-a)|^2-n*a|^(n+1)/(1-a)+n*a|^(n+1)+a|^(n+1)
.=a*(1-a|^(n+1))/(1-a)|^2- (n+1)*a|^(n+2)/(1-a) by A1,Lm6;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=0*a|^0 by A2
.=(1-1)*a/(1-a)|^2-0*a|^(0+1)/(1-a)
.=(1-a|^0)*a/(1-a)|^2-0*a|^(0+1)/(1-a) by NEWTON:4;
then
A4: X[0];
for n holds X[n] from NAT_1:sch 2(A4,A3);
hence thesis;
end;
theorem
(for n holds s.n = 1/((2 -Root (n+1))+(2 -Root n))) implies
Partial_Sums(s).n = 2 -Root (n+1)
proof
defpred X[Nat] means Partial_Sums(s).$1 = 2-Root ($1+1);
assume
A1: for n holds s.n = 1/((2 -Root (n+1))+(2 -Root n));
A2: for n st X[n] holds X[n+1]
proof
let n;
assume Partial_Sums(s).n = 2 -Root (n+1);
then Partial_Sums(s).(n+1) = 2 -Root (n+1)+s.(n+1) by SERIES_1:def 1
.=2 -Root (n+1)+1/((2 -Root ((n+1)+1))+(2 -Root (n+1))) by A1
.=2 -Root (n+1)+((2 -Root (n+2))-(2 -Root (n+1))) by Lm7
.=2 -Root (n+2);
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.=1/((2 -Root (0+1))+(2 -Root 0)) by A1
.=1/((2 -Root (0+1))+0) by PREPOWER:def 2
.=1/1 by PREPOWER:20
.=2 -Root (0+1) by PREPOWER:20;
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/2)|^n) implies for n holds Partial_Sums(s
).n = 2|^(n+1)-(1/2)|^n+1
proof
defpred X[Nat] means Partial_Sums(s).$1 =2|^($1+1)-(1/2)|^$1+1;
assume
A1: for n holds s.n = 2|^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)-(1/2)|^n+1;
then Partial_Sums(s).(n+1) = 2|^(n+1)-(1/2)|^n+1 + s.(n+1) by
SERIES_1:def 1
.= 2|^(n+1)-(1/2)|^n+1 + (2|^(n+1) + (1/2)|^(n+1)) by A1
.= -(1/2)|^n+1 +(1/2)|^(n+1)+2|^(n+1)+2|^(n+1)
.= -(1/2)|^n+1+(1/2)|^n*(1/2)+2|^(n+1)+2|^(n+1) by NEWTON:6
.= -((1/2)|^n*(1/2))+1+2|^(n+1)+2|^(n+1)
.= -(1/2)|^(n+1)+1+2|^(n+1)+2|^(n+1) by NEWTON:6
.= -(1/2)|^(n+1)+1+2|^(n+1)*2
.= -(1/2)|^(n+1)+1+2|^(n+1+1) by NEWTON:6;
hence thesis;
end;
Partial_Sums(s).0 = s.0 by SERIES_1:def 1
.= 2|^0 + (1/2)|^0 by A1
.= 1+ (1/2)|^0 by NEWTON:4
.= 2-1+1 by NEWTON:4
.=2|^(0+1)-1+1
.=2|^(0+1)-(1/2)|^0+1 by NEWTON:4;
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+n/((n+1)!)) implies for n st n>=1 holds
Partial_Sums(s).n = (n+1)!-1/((n+1)!)
proof
defpred X[Nat] means Partial_Sums(s).$1= ($1+1)!-1/(($1+1)!);
assume
A1: for n holds s.n = n!*n+n/((n+1)!);
then
A2: s.0 = 0!*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 = (n+1)!-1/((n+1)!);
Partial_Sums(s).(n+1)= (n+1)!-1/((n+1)!)+ s.(n+1) by A4,SERIES_1:def 1
.= (n+1)!-1/((n+1)!) +((n+1)!*(n+1)+(n+1)/((n+1+1)!)) by A1
.= (n+1)!+(n+1)!*(n+1)-1/((n+1)!) +(n+1)/((n+1+1)!)
.=(n+1)!*(n+1+1)-(1*(n+2))/(((n+1)!)*(n+1+1))+(n+1)/((n+2)!) by
XCMPLX_1:91
.=(n+1)!*(n+1+1)-(1*(n+2))/((n+1+1)!)+(n+1)/((n+2)!) by NEWTON:15
.=(n+1)!*(n+1+1)-((n+2)/((n+1+1)!)-(n+1)/((n+2)!))
.=(n+1)!*(n+1+1)-((n+2)-(n+1))/((n+2)!) by XCMPLX_1:120
.=(n+1+1)!-1/((n+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
.=0+s.1 by A2,SERIES_1:def 1
.= 1!*1+1/((1+1)!) by A1
.= (1+1)!-1+1-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
(a <> 1 & for n st n>=1 holds s.n = (a/(a-1))|^n & s.0=0) implies for
n st n>=1 holds Partial_Sums(s).n = a*((a/(a-1))|^n-1)
proof
defpred X[Nat] means Partial_Sums(s).$1 = a*((a/(a-1))|^$1-1);
assume a<>1;
then
A1: a-1 <> 0;
assume
A2: for n st n>=1 holds s.n = (a/(a-1))|^n & s.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 = a*((a/(a-1))|^n-1);
A5: n+1>=1 by NAT_1:11;
Partial_Sums(s).(n+1) =a*((a/(a-1))|^n-1) + s.(n+1) by A4,
SERIES_1:def 1
.=a*(a/(a-1))|^n-a+(a/(a-1))|^(n+1) by A2,A5
.=a*(a/(a-1))|^n+(a/(a-1))|^(n+1)-a
.=a*(a/(a-1))|^n+(a/(a-1))|^n*(a/(a-1))-a by NEWTON:6
.=(a/(a-1))|^n*(a*1+(a/(a-1)))-a
.=(a/(a-1))|^n*(a*1+a*(1/(a-1)))-a by XCMPLX_1:99
.=(a/(a-1))|^n*(a*(1+1/(a-1)))-a
.=(a/(a-1))|^n*(a*((a-1)/(a-1)+1/(a-1)))-a by A1,XCMPLX_1:60
.=(a/(a-1))|^n*(a*(((a-1)+1)/(a-1)))-a by XCMPLX_1:62
.=a*((a/(a-1))|^n*(a/(a-1)))-a
.=a*((a/(a-1))|^(n+1))-a by NEWTON:6
.=a*((a/(a-1))|^(n+1)-1);
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 A2
.= 0 +(a/(a-1))|^1 by A2
.=a/(a-1)+a-a
.=a*(1/(a-1))+a*1-a by XCMPLX_1:99
.=a*(1/(a-1))+a*((a-1)/(a-1))-a by A1,XCMPLX_1:60
.=a*(1/(a-1)+(a-1)/(a-1))-a
.=a*((1+(a-1))/(a-1))-a by XCMPLX_1:62
.=a*((a/(a-1))-1)
.=a*((a/(a-1))|^1-1);
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 = 2|^n*((3*n-1)/4) & s.0=0) implies for n st
n>=1 holds Partial_Sums(s).n = 2|^n*((3*n-4)/2)+2
proof
defpred X[Nat] means Partial_Sums(s).$1=2|^$1*((3*$1-4)/2)+2;
assume
A1: for n st n>=1 holds s.n = 2|^n*((3*n-1)/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 =2|^n*((3*n-4)/2)+2;
A4: n+1>=1 by NAT_1:11;
Partial_Sums(s).(n+1)=2|^n*((3*n-4)/2)+2+s.(n+1) by A3,SERIES_1:def 1
.=(2|^n*((3*n-4)/2)+2)+(2|^(n+1)*((3*(n+1)-1)/4)) by A1,A4
.=2|^n*((3*n-4)/2)+(2|^(n+1))*((3*n+2)/4)+2
.=2|^n*((3*n-4)/2)+(2|^n*2)*((3*n+2)/4)+2 by NEWTON:6
.=2|^n*2*((3*n-1)/2)+2
.=2|^(n+1)*((3*(n+1)-4)/2)+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
.=0+s.1 by A1
.=2|^1*((3*1-1)/4) by A1
.=2*(1/2)
.=(3-4)/2*2+2
.= (3-4)/2*2|^1+2
.=2|^1*(3*1-4)/2+2;
then
A5: X[1];
for n be Nat st n>=1 holds X[n] from NAT_1:sch 8(A5,A2);
hence thesis;
end;
:: Partial Product of Some Series
theorem
(for n holds s.n = (n+1)/(n+2)) implies (Partial_Product s).n = 1/(n+2 )
proof
defpred X[Nat] means (Partial_Product s).$1 = 1/($1+2);
assume
A1: for n holds s.n = (n+1)/(n+2);
A2: for n st X[n] holds X[n+1]
proof
let n;
assume (Partial_Product s).n = 1/(n+2);
then (Partial_Product s).(n+1) = 1/(n+2)* s.(n+1) by SERIES_3:def 1
.=(1/(n+2))*((n+1+1)/(n+1+2)) by A1
.=1/(n+2)*(n+2)/(n+1+2) by XCMPLX_1:74
.=1/(n+1+2) by XCMPLX_1:106;
hence thesis;
end;
(Partial_Product s).0 = s.0 by SERIES_3:def 1
.= (0+1)/(0+2) by A1
.=1/(0+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 = 1/(n+1)) implies (Partial_Product s).n = 1/((n+1)!)
proof
defpred X[Nat] means (Partial_Product s).$1 = 1/(($1+1)!);
assume
A1: for n holds s.n = 1/(n+1);
A2: for n st X[n] holds X[n+1]
proof
let n;
assume (Partial_Product s).n = 1/((n+1)!);
then (Partial_Product s).(n+1) = 1/((n+1)!)* s.(n+1) by SERIES_3:def 1
.=1/((n+1)!)*(1/(n+1+1)) by A1
.=(1/((n+1)!)*1)/(n+1+1) by XCMPLX_1:74
.= 1/((n+1)!*((n+1)+1)) by XCMPLX_1:78
.= 1/((n+2)!) by NEWTON:15;
hence thesis;
end;
(Partial_Product s).0 = s.0 by SERIES_3:def 1
.= 1/((0+1)!) by A1,NEWTON:13;
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 = n & s.0 = 1) implies for n st n>=1 holds (
Partial_Product s).n = n!
proof
defpred X[Nat] means (Partial_Product s).$1 = $1!;
assume
A1: for n st n>=1 holds s.n= n & s.0 = 1;
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_Product s).n = n!;
A4: n+1>=1 by NAT_1:11;
(Partial_Product s).(n+1)=(Partial_Product s).n*s.(n+1) by
SERIES_3:def 1
.= n!*(n+1) by A1,A3,A4
.= (n+1)! by NEWTON:15;
hence thesis;
end;
(Partial_Product s).(1+0) = (Partial_Product s).0 * s.(1+0) by SERIES_3:def 1
.= s.0 * s.(1+0) by SERIES_3:def 1
.=1*s.1 by A1
.=1! by A1,NEWTON:13;
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 st n>=1 holds s.n = a/n & s.0 = 1) implies for n st n>=1 holds
(Partial_Product s).n = a|^n/(n!)
proof
defpred X[Nat] means (Partial_Product s).$1 = a|^$1/($1!);
assume
A1: for n st n>=1 holds s.n= a/n & s.0 = 1;
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_Product s).n = a|^n/(n!);
A4: n+1>=1 by NAT_1:11;
(Partial_Product s).(n+1)=(Partial_Product s).n*s.(n+1) by
SERIES_3:def 1
.=(a|^n/(n!))*(a/(n+1)) by A1,A3,A4
.=(a|^n*a)/(n!*(n+1)) by XCMPLX_1:76
.=a|^(n+1)/(n!*(n+1)) by NEWTON:6
.=a|^(n+1)/((n+1)!) by NEWTON:15;
hence thesis;
end;
(Partial_Product s).(1+0) = (Partial_Product s).0 * s.(1+0) by SERIES_3:def 1
.= s.0 * s.(1+0) by SERIES_3:def 1
.=1*s.1 by A1
.=1*a/1 by A1
.= a|^1/(1!)by NEWTON:13;
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 st n>=1 holds s.n = a & s.0 = 1) implies for n st n>=1 holds (
Partial_Product s).n = a|^n
proof
defpred X[Nat] means (Partial_Product s).$1 = a|^$1;
assume
A1: for n st n>=1 holds s.n = a & s.0 = 1;
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_Product s).n = a|^n;
A4: n+1>=1 by NAT_1:11;
(Partial_Product s).(n+1)=(Partial_Product s).n*s.(n+1) by
SERIES_3:def 1
.=(a|^n*a) by A1,A3,A4
.=a|^(n+1) by NEWTON:6;
hence thesis;
end;
(Partial_Product s).(1+0) = (Partial_Product s).0 * s.(1+0) by SERIES_3:def 1
.= s.0 * s.(1+0) by SERIES_3:def 1
.=1*s.1 by A1
.=1*a by A1
.= a|^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 st n>=2 holds s.n = 1-1/(n|^2) & s.0 = 1 & s.1 = 1) implies for
n st n>=2 holds (Partial_Product s).n = (n+1)/(2*n)
proof
defpred X[Nat] means (Partial_Product s).$1 = ($1+1)/(2*$1);
assume
A1: for n st n>=2 holds s.n= 1-1/(n|^2) & s.0 = 1 & s.1 = 1;
A2: for n be Nat st n>=2 & X[n] holds X[n+1]
proof
let n be Nat;
assume that
A3: n>=2 and
A4: (Partial_Product s).n = (n+1)/(2*n);
A5: n+1 > 1+1 by A3,NAT_1:13;
(n+1)*(n+1) <> 0;
then
A6: (n+1)|^2 <>0 by WSIERP_1:1;
(Partial_Product s).(n+1)=(Partial_Product s).n*s.(n+1) by
SERIES_3:def 1
.=(n+1)/(2*n)*(1-1/(n+1)|^2) by A1,A4,A5
.=(n+1)/(2*n)*((n+1)|^2/(n+1)|^2-1/(n+1)|^2) by A6,XCMPLX_1:60
.=(n+1)/(2*n)*(((n+1)|^2-1)/(n+1)|^2) by XCMPLX_1:120
.=(n+1)/(2*n)*(((n+1)|^2-1|^2)/(n+1)|^2)
.=(n+1)/(2*n)*((((n+1)-1)*((n+1)+1))/(n+1)|^2) by Lm4
.=((n+1)*((n*(n+2)))/((2*n)*(n+1)|^2)) by XCMPLX_1:76
.=((n+1)*n*(n+2))/(2*n*((n+1)*(n+1))) by WSIERP_1:1
.=(((n+1)*n)*(n+2))/((n*(n+1))*(2*(n+1)))
.=((n+1)*n)/(n*(n+1))*((n+2)/(2*(n+1))) by XCMPLX_1:76
.=((n+1)/(n+1)*(n/n))*((n+2)/(2*(n+1))) by XCMPLX_1:76
.=(1*(n/n))*((n+2)/(2*(n+1))) by XCMPLX_1:60
.=(1*1)*((n+2)/(2*(n+1))) by A3,XCMPLX_1:60
.=(n+2)/(2*(n+1));
hence thesis;
end;
(Partial_Product s).(1+1) = (Partial_Product s).(1+0)*s.2 by SERIES_3:def 1
.= (Partial_Product s).0*s.1*s.2 by SERIES_3:def 1
.=s.0*s.1*s.2 by SERIES_3:def 1
.= 1*s.1*s.2 by A1
.=1*1*s.2 by A1
.= 1- 1/4 by A1,Lm1
.= (2+1)/(2*2);
then
A7: X[2];
for n be Nat st n>=2 holds X[n] from NAT_1:sch 8(A7,A2);
hence thesis;
end;