0 by A4;
then 1/(p * r) > 0;
then 0 < [\1/(p * r)/] + 1 by A6;
then [\1/(p * r)/] is Element of NAT by INT_1:3,7;
then consider m such that
A8: m = [\1/(p * r)/];
take m;
A9: 1/(p * r) = 1/p/r by XCMPLX_1:78;
now
A10: [\1/(p * r)/] > 1/(p * r) -1 by INT_1:def 6;
let n;
assume m<=n;
then n > 1/(p * r) - 1 by A8,A10,XXREAL_0:2;
then n + 1 > 1/p/r by A9,XREAL_1:19;
then
A11: (n+1) * r > 1/p by A4,XREAL_1:77;
0 + (n+1) * r < 1 + (n+1) * r by XREAL_1:6;
then
A12: 1/p < 1 + (n+1) * r by A11,XXREAL_0:2;
A13: (1+r) to_power (n+1) = 1 to_power (n+1) / a to_power (n+1) by A1,POWER:31
.= 1 / a to_power (n+1);
a to_power (n+1) > 0 by A1,POWER:34;
then
A14: |.a to_power (n+1).| = a to_power (n+1) by ABSVALUE:def 1;
1 + (n+1) * r <= (1 + r) to_power (n + 1) by A4,POWER:49;
then 1/p < 1/ a to_power (n+1) by A13,A12,XXREAL_0:2;
then |.a to_power (n+1).| < p by A7,A14,XREAL_1:91;
hence |.s.n - 0.| < p by A3;
end;
hence thesis;
end;
hence s is convergent by SEQ_2:def 6;
hence thesis by A5,SEQ_2:def 7;
end;
theorem Th2:
for n being Nat holds |.a.| to_power n = |.a to_power n.|
proof
let n be Nat;
per cases;
suppose
A1: a <> 0;
then
A2: |.a.| > 0 by COMPLEX1:47;
now
per cases by A1;
suppose a>0;
then a to_power n = |.a.| to_power n & a to_power n > 0
by ABSVALUE:def 1,POWER:34;
hence thesis by ABSVALUE:def 1;
end;
suppose
A3: a < 0;
reconsider m=n as Integer;
now
per cases;
suppose
A4: m is even;
A5: |.a.| to_power n > 0 by A2,POWER:34;
|.a.| to_power n = (-a) to_power m by A3,ABSVALUE:def 1
.= a to_power m by A4,POWER:47;
hence thesis by A5,ABSVALUE:def 1;
end;
suppose
A6: m is odd;
A7: |.a.| to_power n > 0 by A2,POWER:34;
|.a.| to_power n = (-a) to_power m by A3,ABSVALUE:def 1
.= - a to_power m by A6,POWER:48;
hence |.a.| to_power n = |. - a to_power n.|
by A7,ABSVALUE:def 1
.= |. a to_power n.| by COMPLEX1:52;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A8: a = 0;
per cases;
suppose n = 0;
then a to_power n = 1 by NEWTON:4;
hence thesis by A8,COMPLEX1:44,48;
end;
suppose n > 0;
then |.a.| to_power n = 0 by A8,COMPLEX1:44,POWER:def 2;
hence thesis by A8,COMPLEX1:44;
end;
end;
end;
theorem Th3:
|.a.|<1 & (for n holds s.n=a to_power (n+1)) implies s is
convergent & lim s = 0
proof
assume that
A1: |.a.| < 1 and
A2: for n holds s.n=a to_power (n+1);
now
per cases;
suppose
|.a.| = 0;
then
A3: a = 0 by ABSVALUE:2;
now
let n be Nat;
n in NAT & a to_power (n+1) = 0 by A3,ORDINAL1:def 12,POWER:def 2;
hence s.n = In(0,REAL) by A2;
end;
then s is constant & s.0 = In(0,REAL);
hence thesis by SEQ_4:26;
end;
suppose
A4: not |.a.| = 0;
deffunc U(Nat) = |.a.| to_power ($1+1);
consider s1 such that
A5: for n holds s1.n = U(n) from SEQ_1:sch 1;
A6: now
let n;
thus s1.n = |.a.| to_power (n+1) by A5
.= |.a to_power (n+1).| by Th2
.= |.s.n.| by A2;
end;
A7: |.a.| > 0 by A4,COMPLEX1:46;
then lim s1 = 0 by A1,A5,Th1;
then
A8: lim abs(s) = 0 by A6,SEQ_1:12;
s1 is convergent by A1,A7,A5,Th1;
then abs(s) is convergent by A6,SEQ_1:12;
hence thesis by A8,SEQ_4:15;
end;
end;
hence thesis;
end;
definition
let X be non empty add-closed complex-membered set;
let s1, s2 be sequence of X;
redefine func s1+s2 -> sequence of X;
coherence
proof
A1: dom(s1+s2) = dom s1 /\ dom s2 by VALUED_1:def 1
.= NAT /\ dom s2 by FUNCT_2:def 1
.= NAT /\ NAT by FUNCT_2:def 1;
now
let x be object such that
A2: x in NAT;
A3: s1.x in X & s2.x in X by A2,FUNCT_2:5;
(s1+s2).x = s1.x + s2.x by A1,A2,VALUED_1:def 1;
hence (s1+s2).x in X by A3,MEMBERED:def 25;
end;
hence thesis by A1,FUNCT_2:3;
end;
end;
definition
let s be complex-valued ManySortedSet of NAT;
func Partial_Sums(s) -> complex-valued ManySortedSet of NAT means
:Def1:
it.0 = s.0 & for n holds it.(n+1) = it.n + s.(n+1);
existence
proof
set X = COMPLEX;
A1: dom s = NAT by PARTFUN1:def 2;
rng s c= X by VALUED_0:def 1;
then reconsider ss = s as sequence of X by A1,RELSET_1:4;
defpred P[Nat,Element of X,set] means $3 = $2 + ss.($1+1);
A2: for n being Nat for x being Element of X
ex y being Element of X st P[n,x,y]
proof let n be Nat, x be Element of X;
reconsider y = x + ss.(n+1) as Element of COMPLEX by XCMPLX_0:def 2;
take y;
thus thesis;
end;
consider f being sequence of X such that
A3: f.0 = ss.0 and
A4: for n being Nat holds P[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(A2);
take f;
thus f.0 = s.0 by A3;
let n;
reconsider n as Element of NAT by ORDINAL1:def 12;
P[n,f.n,f.(n+1)] by A4;
hence thesis;
end;
uniqueness
proof
let s1,s2 be complex-valued ManySortedSet of NAT;
assume that
A5: s1.0=s.0 and
A6: for n holds s1.(n+1)=s1.n + s.(n+1) and
A7: s2.0=s.0 and
A8: for n holds s2.(n+1)=s2.n + s.(n+1);
defpred X[Nat] means s1.$1 = s2.$1;
A9: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
assume s1.k =s2.k;
hence s1.(k+1) = s2.k + s.(k+1) by A6
.= s2.(k+1) by A8;
end;
A10: X[0] by A5,A7;
for n being Nat holds X[n] from NAT_1:sch 2(A10,A9);
hence thesis;
end;
end;
registration
let s be real-valued ManySortedSet of NAT;
cluster Partial_Sums s -> real-valued;
coherence
proof set f = Partial_Sums s;
let x be object;
assume
x in dom f;
then reconsider n = x as Element of NAT;
defpred P[Nat] means f.$1 is real;
f.0 = s.0 by Def1;
then
A1: P[0];
A2: for k be Nat st P[k] holds P[k + 1]
proof let k be Nat;
assume
A3: P[k];
reconsider k as Element of NAT by ORDINAL1:def 12;
f.(k+1) = f.k + s.(k+1) by Def1;
hence thesis by A3;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
then f.n is real;
hence thesis;
end;
end;
definition
let s be Real_Sequence;
redefine func Partial_Sums s -> Real_Sequence;
coherence
proof
A1: dom Partial_Sums s = NAT by PARTFUN1:def 2;
rng Partial_Sums s c= REAL by VALUED_0:def 3;
then Partial_Sums s is Relation of NAT, REAL by A1,RELSET_1:4;
hence Partial_Sums s is Real_Sequence;
end;
end;
definition
let s;
attr s is summable means
:Def2:
Partial_Sums(s) is convergent;
func Sum(s) -> Real equals
lim Partial_Sums(s);
correctness;
end;
theorem Th4:
s is summable implies s is convergent & lim s = 0
proof
assume s is summable;
then
A1: Partial_Sums(s) is convergent;
now
let n;
(Partial_Sums(s)).(n+1) = (Partial_Sums(s)).n + s.(n+1) by Def1;
then (Partial_Sums(s)).(n+1) = (Partial_Sums(s)).n + (s ^\1).n by
NAT_1:def 3;
hence (Partial_Sums(s) ^\1).n = (Partial_Sums(s)).n + (s ^\1).n by
NAT_1:def 3;
end;
then
A2: (Partial_Sums(s) ^\1) = Partial_Sums(s) + s ^\1 by SEQ_1:7;
now
let n be Element of NAT;
thus (s ^\1 + (Partial_Sums(s) - Partial_Sums(s))).n = (s ^\1).n + (
Partial_Sums(s) +- Partial_Sums(s)).n by SEQ_1:7
.= (s ^\1).n + ((Partial_Sums(s)).n + (-Partial_Sums(s)).n) by SEQ_1:7
.= (s ^\1).n + ((Partial_Sums(s)).n +- (Partial_Sums(s)).n) by SEQ_1:10
.= (s ^\1).n;
end;
then s ^\1 + (Partial_Sums(s) - Partial_Sums(s)) = s ^\1;
then
A3: s ^\1 = Partial_Sums(s) ^\1 - Partial_Sums(s) by A2,SEQ_1:31;
then
A4: s ^\1 qua Real_Sequence is convergent by A1;
hence s is convergent by SEQ_4:21;
lim(Partial_Sums(s) ^\1) = lim(Partial_Sums(s)) by A1,SEQ_4:20;
then
lim(Partial_Sums(s) ^\1 - Partial_Sums(s)) = lim(Partial_Sums(s)) - lim(
Partial_Sums(s)) by A1,SEQ_2:12
.= 0;
hence thesis by A3,A4,SEQ_4:22;
end;
Lm1:
for seq,seq1,seq2 being complex-valued ManySortedSet of NAT holds
seq = seq1 + seq2 iff for n holds seq.n =seq1.n + seq2.n
proof
let seq,seq1,seq2 be complex-valued ManySortedSet of NAT;
thus seq = seq1 + seq2 implies for n holds seq.n =seq1.n + seq2.n
proof
assume
A1: seq = seq1 + seq2;
let n;
A2: n in NAT by ORDINAL1:def 12;
dom seq = NAT by PARTFUN1:def 2;
hence thesis by A1,VALUED_1:def 1,A2;
end;
assume for n holds seq.n =seq1.n + seq2.n;
then
A3: for n being object st n in dom seq holds seq.n = seq1.n + seq2.n;
dom seq = NAT /\ NAT by PARTFUN1:def 2
.= NAT /\ dom seq2 by PARTFUN1:def 2
.= dom seq1 /\ dom seq2 by PARTFUN1:def 2;
hence thesis by A3,VALUED_1:def 1;
end;
theorem Th5:
for X being non empty add-closed complex-membered set
for s1,s2 being sequence of X holds
Partial_Sums(s1) + Partial_Sums(s2) = Partial_Sums(s1+s2)
proof
let X be non empty add-closed complex-membered set;
let s1,s2 be sequence of X;
A1: now
let n;
thus (Partial_Sums(s1) + Partial_Sums(s2)).(n+1) = Partial_Sums(s1).(n+1)
+ Partial_Sums(s2).(n+1) by Lm1
.= Partial_Sums(s1).n + s1.(n+1) + Partial_Sums(s2).(n+1) by Def1
.= Partial_Sums(s1).n+s1.(n+1)+(s2.(n+1)+Partial_Sums(s2).n) by Def1
.= Partial_Sums(s1).n+(s1.(n+1)+s2.(n+1))+Partial_Sums(s2).n
.= Partial_Sums(s1).n+(s1+s2).(n+1)+Partial_Sums(s2).n by Lm1
.= Partial_Sums(s1).n+Partial_Sums(s2).n+(s1+s2).(n+1)
.= (Partial_Sums(s1)+Partial_Sums(s2)).n+(s1+s2).(n+1) by Lm1;
end;
(Partial_Sums(s1) + Partial_Sums(s2)).0 = Partial_Sums(s1).0 +
Partial_Sums(s2).0 by Lm1
.= s1.0 + Partial_Sums(s2).0 by Def1
.= s1.0 + s2.0 by Def1
.= (s1+s2).0 by Lm1;
hence thesis by A1,Def1;
end;
theorem Th6:
Partial_Sums(s1) - Partial_Sums(s2) = Partial_Sums(s1-s2)
proof
A1: now
let n;
thus (Partial_Sums(s1) - Partial_Sums(s2)).(n+1) = Partial_Sums(s1).(n+1)
- Partial_Sums(s2).(n+1) by RFUNCT_2:1
.= (Partial_Sums(s1).n + s1.(n+1)) - Partial_Sums(s2).(n+1) by Def1
.= (Partial_Sums(s1).n+s1.(n+1))-(s2.(n+1)+Partial_Sums(s2).n) by Def1
.= Partial_Sums(s1).n+(s1.(n+1)-s2.(n+1))-Partial_Sums(s2).n
.= (s1-s2).(n+1)+Partial_Sums(s1).n-Partial_Sums(s2).n by RFUNCT_2:1
.= (s1-s2).(n+1)+(Partial_Sums(s1).n-Partial_Sums(s2).n)
.= (Partial_Sums(s1)-Partial_Sums(s2)).n+(s1-s2).(n+1) by RFUNCT_2:1;
end;
(Partial_Sums(s1) - Partial_Sums(s2)).0 = Partial_Sums(s1).0 -
Partial_Sums(s2).0 by RFUNCT_2:1
.= s1.0 - Partial_Sums(s2).0 by Def1
.= s1.0 - s2.0 by Def1
.= (s1-s2).0 by RFUNCT_2:1;
hence thesis by A1,Def1;
end;
theorem
s1 is summable & s2 is summable implies s1+s2 is summable &
Sum(s1+s2) = Sum(s1) + Sum(s2)
proof
assume s1 is summable & s2 is summable;
then
A1: Partial_Sums(s1) is convergent & Partial_Sums(s2) is convergent;
then Partial_Sums(s1) + Partial_Sums(s2) is convergent;
then Partial_Sums(s1+s2) is convergent by Th5;
hence s1+s2 is summable;
thus Sum(s1+s2) =lim (Partial_Sums(s1) + Partial_Sums(s2)) by Th5
.=Sum(s1) + Sum(s2) by A1,SEQ_2:6;
end;
theorem
s1 is summable & s2 is summable implies s1-s2 is summable & Sum(s1-s2)
= Sum(s1) - Sum(s2)
proof
assume s1 is summable & s2 is summable;
then
A1: Partial_Sums(s1) is convergent & Partial_Sums(s2) is convergent;
then Partial_Sums(s1) - Partial_Sums(s2) is convergent;
then Partial_Sums(s1-s2) is convergent by Th6;
hence s1-s2 is summable;
thus Sum(s1-s2) =lim (Partial_Sums(s1) - Partial_Sums(s2)) by Th6
.=Sum(s1) - Sum(s2) by A1,SEQ_2:12;
end;
theorem Th9:
Partial_Sums(r(#)s) = r(#)Partial_Sums(s)
proof
A1: now
let n;
thus (r(#)Partial_Sums(s)).(n+1) = r*Partial_Sums(s).(n+1) by SEQ_1:9
.= r*(Partial_Sums(s).n + s.(n+1)) by Def1
.= r*Partial_Sums(s).n + r*s.(n+1)
.= (r(#)Partial_Sums(s)).n + r*s.(n+1) by SEQ_1:9
.= (r(#)Partial_Sums(s)).n + (r(#)s).(n+1) by SEQ_1:9;
end;
(r(#)Partial_Sums(s)).0 = r*Partial_Sums(s).0 by SEQ_1:9
.= r*s.0 by Def1
.= (r(#)s).0 by SEQ_1:9;
hence thesis by A1,Def1;
end;
theorem Th10:
s is summable implies r(#)s is summable & Sum(r(#)s) =r*Sum(s)
proof
assume s is summable;
then
A1: Partial_Sums(s) is convergent;
then r(#)Partial_Sums(s) is convergent;
then Partial_Sums(r(#)s) is convergent by Th9;
hence r(#)s is summable;
thus Sum(r(#)s) =lim (r(#)Partial_Sums(s)) by Th9
.=r*Sum(s) by A1,SEQ_2:8;
end;
theorem Th11:
for s,s1 st for n holds s1.n=s.0 holds Partial_Sums(s^\1) = (
Partial_Sums(s)^\1) - s1
proof
let s,s1;
assume
A1: for n holds s1.n=s.0;
A2: now
let k;
thus ((Partial_Sums(s)^\1) - s1).(k+1) = (Partial_Sums(s)^\1).(k+1) - s1.(
k+1) by RFUNCT_2:1
.= (Partial_Sums(s)^\1).(k+1) - s.0 by A1
.= Partial_Sums(s).(k+1+1) - s.0 by NAT_1:def 3
.= s.(k+1+1) + Partial_Sums(s).(k+1) - s.0 by Def1
.= s.(k+1+1) + Partial_Sums(s).(k+1) - s1.k by A1
.= s.(k+1+1) + (Partial_Sums(s).(k+1) - s1.k)
.= s.(k+1+1) + ((Partial_Sums(s)^\1).k - s1.k) by NAT_1:def 3
.= s.(k+1+1) + ((Partial_Sums(s)^\1) - s1).k by RFUNCT_2:1
.= ((Partial_Sums(s)^\1) - s1).k + (s^\1).(k+1) by NAT_1:def 3;
end;
((Partial_Sums(s)^\1) - s1).0 = (Partial_Sums(s)^\1).0 - s1.0 by RFUNCT_2:1
.= (Partial_Sums(s)^\1).0 - s.0 by A1
.= Partial_Sums(s).(0+1) - s.0 by NAT_1:def 3
.= Partial_Sums(s).0 + s.(0+1) - s.0 by Def1
.= s.(0+1) + s.0 - s.0 by Def1
.= (s^\1).0 by NAT_1:def 3;
hence thesis by A2,Def1;
end;
theorem Th12:
s is summable implies for n holds s^\n is summable
proof
defpred X[Nat] means s^\$1 is summable;
A1: for n st X[n] holds X[n+1]
proof
let n;
set s1 = seq_const((s^\n).0);
for k holds s1.k = (s^\n).0 by SEQ_1:57;
then
A2: Partial_Sums(s^\n^\1) = (Partial_Sums(s^\n)^\1) - s1 by Th11;
assume s^\n is summable;
then Partial_Sums(s^\n) is convergent;
then s^\(n+1)=(s^\n)^\1 & Partial_Sums(s^\n^\1) is convergent by A2,
NAT_1:48;
hence thesis by Def2;
end;
assume s is summable;
then
A3: X[0] by NAT_1:47;
thus for n holds X[n] from NAT_1:sch 2(A3,A1);
end;
theorem Th13:
(ex n st s^\n is summable) implies s is summable
proof
given n such that
A1: s^\n is summable;
reconsider PS = Partial_Sums(s).n as Element of REAL;
set s1 = seq_const Partial_Sums(s).n;
for k holds (Partial_Sums(s)^\(n+1)).k = Partial_Sums(s^\(n+1)).k + s1.k
proof
defpred X[Nat] means
(Partial_Sums(s)^\(n+1)).$1 = Partial_Sums
(s^\(n+1)).$1 + s1.$1;
A2: Partial_Sums(s^\(n+1)).0 = (s^\(n+1)).0 by Def1
.= s.(0+(n+1)) by NAT_1:def 3
.= s.(n+1);
A3: for k st X[k] holds X[k+1]
proof
let k;
assume
A4: (Partial_Sums(s)^\(n+1)).k = Partial_Sums(s^\(n+1)).k + s1.k;
Partial_Sums(s^\(n+1)).(k+1) + s1.(k+1) = s1.(k+1) + (Partial_Sums(
s^\(n+1)).k + (s^\(n+1)).(k+1)) by Def1
.= s1.(k+1) + Partial_Sums(s^\(n+1)).k + (s^\(n+1)).(k+1)
.= Partial_Sums(s).n + Partial_Sums(s^\(n+1)).k + (s^\(n+1)).(k+1)
by SEQ_1:57
.= (Partial_Sums(s)^\(n+1)).k + (s^\(n+1)).(k+1) by A4,SEQ_1:57
.= Partial_Sums(s).(k+(n+1)) + (s^\(n+1)).(k+1) by NAT_1:def 3
.= Partial_Sums(s).(k+(n+1)) + s.(k+1+(n+1)) by NAT_1:def 3
.= Partial_Sums(s).(k+(n+1)+1) by Def1
.= Partial_Sums(s).(k+1+(n+1))
.= (Partial_Sums(s)^\(n+1)).(k+1) by NAT_1:def 3;
hence thesis;
end;
(Partial_Sums(s)^\(n+1)).0 = Partial_Sums(s).(0+(n+1)) by NAT_1:def 3
.= s.(n+1) + Partial_Sums(s).n by Def1
.= Partial_Sums(s^\(n+1)).0 + s1.0 by A2,SEQ_1:57;
then
A5: X[0];
thus for k holds X[k] from NAT_1:sch 2(A5,A3);
end;
then
A6: Partial_Sums(s)^\(n+1) = Partial_Sums(s^\(n+1)) + s1 by SEQ_1:7
.= Partial_Sums((s^\n)^\1) + s1 by NAT_1:48;
s^\n^\1 is summable by A1,Th12;
then Partial_Sums(s^\n^\1) is convergent;
then Partial_Sums(s)^\(n+1) is convergent by A6;
then Partial_Sums(s) is convergent by SEQ_4:21;
hence thesis;
end;
theorem Th14:
(for n holds s1.n<=s2.n) implies for n holds Partial_Sums(s1).n
<=Partial_Sums(s2).n
proof
defpred X[Nat] means
Partial_Sums(s1).$1 <= Partial_Sums(s2).$1;
assume
A1: for n holds s1.n<=s2.n;
A2: for n st X[n] holds X[n+1]
proof
let n such that
A3: Partial_Sums(s1).n <= Partial_Sums(s2).n;
A4: s1.(n+1)<=s2.(n+1) by A1;
Partial_Sums(s1).(n+1) = Partial_Sums(s1).n + s1.(n+1) & Partial_Sums(
s2).(n +1) = Partial_Sums(s2).n + s2.(n+1) by Def1;
hence thesis by A3,A4,XREAL_1:7;
end;
Partial_Sums(s2).0 = s2.0 & Partial_Sums(s1).0 = s1.0 by Def1;
then
A5: X[0] by A1;
thus for n holds X[n] from NAT_1:sch 2(A5,A2);
end;
theorem
s is summable implies
for n holds Sum(s) = Partial_Sums(s).n + Sum(s^\(n+1))
proof
defpred X[Nat] means
Sum(s) = Partial_Sums(s).$1 + Sum(s^\($1+1));
assume
A1: s is summable;
A2: for n st X[n] holds X[n+1]
proof
let n;
assume
A3: Sum(s) = Partial_Sums(s).n + Sum(s^\(n+1));
set s1 = seq_const (s^\(n+1)).0;
for k holds s1.k= (s^\(n+1)).0 by SEQ_1:57;
then
A4: Partial_Sums(s^\(n+1)^\1) = (Partial_Sums(s^\(n+1))^\1) - s1 by Th11;
s^\(n+1) is summable by A1,Th12;
then
A5: Partial_Sums(s^\(n+1)) is convergent;
lim Partial_Sums(s^\(n+1+1)) = lim Partial_Sums(s^\(n+1)^\1) by NAT_1:48
.= lim (Partial_Sums(s^\(n+1))^\1) - lim s1 by A5,A4,SEQ_2:12
.= lim Partial_Sums(s^\(n+1)) - lim s1 by A5,SEQ_4:20
.= Sum(s^\(n+1)) - s1.0 by SEQ_4:26
.= Sum(s^\(n+1)) - (s^\(n+1)).0 by SEQ_1:57;
then Sum(s^\(n+1+1)) = Sum(s) - (Partial_Sums(s).n + (s^\(n+1)).0) by A3
.= Sum(s) - (Partial_Sums(s).n + s.(0+(n+1))) by NAT_1:def 3
.= Sum(s) - Partial_Sums(s).(n+1) by Def1;
hence thesis;
end;
A6: X[0]
proof
set s1 = seq_const s.0;
A7: Partial_Sums(s) is convergent by A1;
for k holds s1.k= s.0 by SEQ_1:57;
then Partial_Sums(s^\1) = (Partial_Sums(s)^\1) - s1 by Th11;
then lim Partial_Sums(s^\1) = lim (Partial_Sums(s)^\1) - lim s1 by A7,
SEQ_2:12
.= lim Partial_Sums(s) - lim s1 by A7,SEQ_4:20
.= Sum(s) - s1.0 by SEQ_4:26
.= Sum(s) - s.0 by SEQ_1:57;
then Sum(s) = Sum(s^\1) +(-(-s.0));
hence thesis by Def1;
end;
thus for n holds X[n] from NAT_1:sch 2(A6,A2);
end;
theorem Th16:
(for n holds 0<=s.n) implies Partial_Sums(s) is non-decreasing
proof
assume
A1: for n holds 0<=s.n;
now
let n;
0<=s.(n+1) by A1;
then 0 + Partial_Sums(s).n <= s.(n+1) + Partial_Sums(s).n by XREAL_1:6;
hence Partial_Sums(s).n <= Partial_Sums(s).(n+1) by Def1;
end;
hence thesis;
end;
theorem Th17:
(for n holds 0<=s.n) implies (Partial_Sums(s) is bounded_above
iff s is summable)
proof
assume for n holds 0<=s.n;
then Partial_Sums(s) is non-decreasing by Th16;
hence Partial_Sums(s) is bounded_above implies s is summable;
assume s is summable;
then Partial_Sums(s) is convergent;
then Partial_Sums(s) is bounded;
hence thesis;
end;
theorem
s is summable & (for n holds 0<=s.n) implies 0<=Sum(s)
proof
assume that
A1: s is summable and
A2: for n holds 0<=s.n;
A3: now
let n;
A4: Partial_Sums(s).0 = s.0 by Def1;
Partial_Sums(s).0<=Partial_Sums(s).n & 0<=s.0 by A2,Th16,SEQM_3:11;
hence 0<=Partial_Sums(s).n by A4;
end;
Partial_Sums(s) is convergent by A1;
hence thesis by A3,SEQ_2:17;
end;
theorem Th19:
(for n holds 0<=s2.n) & s1 is summable & (ex m st for n st m<=n
holds s2.n<=s1.n) implies s2 is summable
proof
assume that
A1: for n holds 0<=s2.n and
A2: s1 is summable;
given m such that
A3: for n st m<=n holds s2.n<=s1.n;
s1^\m is summable by A2,Th12;
then Partial_Sums(s1^\m) is bounded_above;
then consider r being Real such that
A4: for n holds Partial_Sums(s1^\m).n