let a be NAT -valued Real_Sequence; :: thesis: for b, c, n being Nat st b >= 2 & c >= 1 & rng a c= c & c <= b holds
Sum ((Liouville_seq (a,b)) ^\ (n + 1)) <= Sum ((c - 1) (#) ((powerfact b) ^\ (n + 1)))
let b, c, n be Nat; :: thesis: ( b >= 2 & c >= 1 & rng a c= c & c <= b implies Sum ((Liouville_seq (a,b)) ^\ (n + 1)) <= Sum ((c - 1) (#) ((powerfact b) ^\ (n + 1))) )
set g = (c - 1) (#) ((powerfact b) ^\ (n + 1));
assume A0: ( b >= 2 & c >= 1 & rng a c= c & c <= b ) ; :: thesis: Sum ((Liouville_seq (a,b)) ^\ (n + 1)) <= Sum ((c - 1) (#) ((powerfact b) ^\ (n + 1)))
then b >= 1 + 1 ;
then b > 1 by NAT_1:13;
then (powerfact b) ^\ (n + 1) is summable by Th26, SERIES_1:12;
then A1: (c - 1) (#) ((powerfact b) ^\ (n + 1)) is summable by SERIES_1:10;
set f = (Liouville_seq (a,b)) ^\ (n + 1);
A2: b is 2 _or_greater by A0, EC_PF_2:def 1;
A3: for i being Nat holds 0 <= ((Liouville_seq (a,b)) ^\ (n + 1)) . i
proof
let i be Nat; :: thesis: 0 <= ((Liouville_seq (a,b)) ^\ (n + 1)) . i
dom ((Liouville_seq (a,b)) ^\ (n + 1)) = NAT by FUNCT_2:def 1;
then ((Liouville_seq (a,b)) ^\ (n + 1)) . i in rng ((Liouville_seq (a,b)) ^\ (n + 1)) by FUNCT_1:3, ORDINAL1:def 12;
hence 0 <= ((Liouville_seq (a,b)) ^\ (n + 1)) . i by A2, PARTFUN3:def 4; :: thesis: verum
end;
for i being Nat holds ((Liouville_seq (a,b)) ^\ (n + 1)) . i <= ((c - 1) (#) ((powerfact b) ^\ (n + 1))) . i
proof
let i be Nat; :: thesis: ((Liouville_seq (a,b)) ^\ (n + 1)) . i <= ((c - 1) (#) ((powerfact b) ^\ (n + 1))) . i
A4: ((Liouville_seq (a,b)) ^\ (n + 1)) . i = (Liouville_seq (a,b)) . ((n + 1) + i) by NAT_1:def 3;
((c - 1) (#) ((powerfact b) ^\ (n + 1))) . i = (c - 1) * (((powerfact b) ^\ (n + 1)) . i) by SEQ_1:9
.= (c - 1) * ((powerfact b) . ((n + 1) + i)) by NAT_1:def 3
.= ((c - 1) (#) (powerfact b)) . ((n + 1) + i) by SEQ_1:9 ;
hence ((Liouville_seq (a,b)) ^\ (n + 1)) . i <= ((c - 1) (#) ((powerfact b) ^\ (n + 1))) . i by A4, Th34, A0; :: thesis: verum
end;
hence Sum ((Liouville_seq (a,b)) ^\ (n + 1)) <= Sum ((c - 1) (#) ((powerfact b) ^\ (n + 1))) by SERIES_1:20, A1, A3; :: thesis: verum