:: Partial Sum of Some Series
:: by Ming Liang and Yuzhong Ding
::
:: Received September 25, 2004
:: Copyright (c) 2004-2016 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;