let a be NAT -valued Real_Sequence; :: thesis: for b, c being Nat st b >= 2 & c >= 1 & rng a c= c & c <= b holds
Sum (Liouville_seq (a,b)) <= Sum ((c - 1) (#) (powerfact b))
let b, c be Nat; :: thesis: ( b >= 2 & c >= 1 & rng a c= c & c <= b implies Sum (Liouville_seq (a,b)) <= Sum ((c - 1) (#) (powerfact b)) )
assume A0: ( b >= 2 & c >= 1 & rng a c= c & c <= b ) ; :: thesis: Sum (Liouville_seq (a,b)) <= Sum ((c - 1) (#) (powerfact b))
then b >= 1 + 1 ;
then b > 1 by NAT_1:13;
then powerfact b is summable by Th26;
then A1: (c - 1) (#) (powerfact b) is summable by SERIES_1:10;
b is 2 _or_greater by A0, EC_PF_2:def 1;
then A2: for i being Nat holds 0 <= (Liouville_seq (a,b)) . i by Th33;
for i being Nat holds (Liouville_seq (a,b)) . i <= ((c - 1) (#) (powerfact b)) . i by Th34, A0;
hence Sum (Liouville_seq (a,b)) <= Sum ((c - 1) (#) (powerfact b)) by SERIES_1:20, A1, A2; :: thesis: verum