:: Partial Sum of Some Series :: by Ming Liang and Yuzhong Ding :: :: Received September 25, 2004 :: Copyright (c) 2004-2017 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, XCMPLX_0, INT_1; requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE; 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 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;