:: Partial Sum and Partial Product of Some Series :: by Jianbing Cao , Fahui Zhai and Xiquan Liang :: :: Received November 7, 2005 :: Copyright (c) 2005-2021 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; begin reserve n for Nat, a,b,c,d for Real, s for Real_Sequence; theorem :: SERIES_4:1 (a+b+c)|^2=a|^2+b|^2+c|^2+2*a*b+2*a*c+2*b*c; theorem :: SERIES_4:2 (a+b)|^3 = a|^3+3*a|^2*b+3*b|^2*a+b|^3; theorem :: SERIES_4:3 (a-b+c)|^2=a|^2+b|^2+c|^2-2*a*b+2*a*c-2*b*c; theorem :: SERIES_4:4 (a-b-c)|^2=a|^2+b|^2+c|^2-2*a*b-2*a*c+2*b*c; theorem :: SERIES_4:5 (a-b)|^3 = a|^3-3*a|^2*b+3*b|^2*a-b|^3; theorem :: SERIES_4:6 (a+b)|^4 = a|^4+4*a|^3*b+6*a|^2*b|^2+4*b|^3*a+b|^4; theorem :: SERIES_4:7 (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; theorem :: SERIES_4:8 (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; theorem :: SERIES_4:9 a<>0 implies ((1/a)|^(n+1)+a|^(n+1))|^2 = (1/a)|^(2*n+2)+a|^(2*n+2)+2; :: Geometrical Series theorem :: SERIES_4:10 (a <> 1 & for n holds s.n = a|^n) implies Partial_Sums(s).n = (1 - a|^ (n+1))/(1-a); theorem :: SERIES_4:11 (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); :: Compositive Series theorem :: SERIES_4:12 (for n holds s.n = 10|^n+2*n+1) implies Partial_Sums(s).n = 10|^(n+1)/ 9-1/9+(n+1)|^2; theorem :: SERIES_4:13 (for n holds s.n = 2*n-1+(1/2)|^n) implies Partial_Sums(s).n =n|^2+1-( 1/2)|^n; theorem :: SERIES_4:14 (for n holds s.n = n*(1/2)|^n) implies Partial_Sums(s).n =2-(2+n)*(1/2 )|^n; theorem :: SERIES_4:15 (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; theorem :: SERIES_4:16 (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; theorem :: SERIES_4:17 (for n holds s.n = n*2|^n) implies for n holds Partial_Sums(s).n = n*2 |^(n+1)-2|^(n+1)+2; theorem :: SERIES_4:18 (for n holds s.n = (2*n+1)*3|^n) implies for n holds Partial_Sums(s).n = n*3|^(n+1)+1; theorem :: SERIES_4:19 (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); theorem :: SERIES_4:20 (for n holds s.n = 1/((2 -Root (n+1))+(2 -Root n))) implies Partial_Sums(s).n = 2 -Root (n+1); theorem :: SERIES_4:21 (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; theorem :: SERIES_4:22 (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)!); theorem :: SERIES_4:23 (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); theorem :: SERIES_4:24 (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; :: Partial Product of Some Series theorem :: SERIES_4:25 (for n holds s.n = (n+1)/(n+2)) implies (Partial_Product s).n = 1/(n+2 ); theorem :: SERIES_4:26 (for n holds s.n = 1/(n+1)) implies (Partial_Product s).n = 1/((n+1)!); theorem :: SERIES_4:27 (for n st n>=1 holds s.n = n & s.0 = 1) implies for n st n>=1 holds ( Partial_Product s).n = n!; theorem :: SERIES_4:28 (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!); theorem :: SERIES_4:29 (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; theorem :: SERIES_4:30 (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);