:: Partial Sum of Some Series :: by Ming Liang and Yuzhong Ding :: :: Received September 25, 2004 :: Copyright (c) 2004-2018 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; begin reserve n for Nat, a,b for Real, s for Real_Sequence; theorem :: SERIES_2:1 |.(-1)|^n.| = 1; theorem :: SERIES_2:2 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 ; theorem :: SERIES_2:3 (for n holds s.n = n) implies for n holds Partial_Sums(s).n = n*(n+1)/ 2; theorem :: SERIES_2:4 (for n holds s.n = 2*n) implies for n holds Partial_Sums(s).n = n*(n+1 ); theorem :: SERIES_2:5 (for n holds s.n = 2*n+1) implies for n holds Partial_Sums(s).n = (n+1 )|^2; theorem :: SERIES_2:6 (for n holds s.n = n*(n+1)) implies for n holds Partial_Sums(s).n = n* (n+1)*(n+2)/3; theorem :: SERIES_2:7 (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; theorem :: SERIES_2:8 (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; theorem :: SERIES_2:9 (for n holds s.n = 1/(n*(n+1))) implies for n holds Partial_Sums(s).n = 1-1/(n+1); theorem :: SERIES_2:10 (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)); theorem :: SERIES_2:11 (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)); theorem :: SERIES_2:12 (for n holds s.n = n |^ 2) implies for n holds Partial_Sums(s).n = n*( n+1)*(2*n+1)/6; theorem :: SERIES_2:13 (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; theorem :: SERIES_2:14 (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; theorem :: SERIES_2:15 (for n holds s.n = n |^ 3) implies for n holds Partial_Sums(s).n = n|^ 2*(n+1)|^2/4; theorem :: SERIES_2:16 (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); theorem :: SERIES_2:17 (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; theorem :: SERIES_2:18 (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; theorem :: SERIES_2:19 (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; theorem :: SERIES_2:20 (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; theorem :: SERIES_2:21 (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; theorem :: SERIES_2:22 (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; theorem :: SERIES_2:23 (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; theorem :: SERIES_2:24 (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; theorem :: SERIES_2:25 (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)); theorem :: SERIES_2:26 (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); theorem :: SERIES_2:27 (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); theorem :: SERIES_2:28 (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)); theorem :: SERIES_2:29 (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)); theorem :: SERIES_2:30 (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)); theorem :: SERIES_2:31 (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)); theorem :: SERIES_2:32 (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; theorem :: SERIES_2:33 (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)); theorem :: SERIES_2:34 (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); theorem :: SERIES_2:35 (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); theorem :: SERIES_2:36 (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))); theorem :: SERIES_2:37 (for n holds s.n = n!*n) implies for n st n>=1 holds Partial_Sums(s).n = (n+1)!-1; theorem :: SERIES_2:38 (for n holds s.n = n/((n+1)!)) implies for n st n>=1 holds Partial_Sums(s).n = 1-1/((n+1)!); theorem :: SERIES_2:39 (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)!); theorem :: SERIES_2:40 (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)!); :: Added by AG, 5.09.2005 theorem :: SERIES_2:41 (for n holds s.n = a*n+b) implies for n holds Partial_Sums(s).n = a*(n +1)*n/2+n*b+b; ::\$N Sum of an arithmetic series theorem :: SERIES_2:42 (for n holds s.n = a*n+b) implies for n holds Partial_Sums(s).n = (n+1 )*(s.0 + s.n)/2;