let a be NAT -valued Real_Sequence; :: thesis: for b being non zero Nat st b >= 2 & rng a c= b holds
Liouville_seq (a,b) is summable
let b be non zero Nat; :: thesis: ( b >= 2 & rng a c= b implies Liouville_seq (a,b) is summable )
assume A1: ( b >= 2 & rng a c= b ) ; :: thesis: Liouville_seq (a,b) is summable
A2: b > 1 by A1, XXREAL_0:2;
then A3: b - 1 >= 0 by XREAL_1:48;
set f = Liouville_seq (a,b);
A4: for i being Nat holds (b - 1) / (b to_power (i !)) = ((b - 1) (#) (powerfact b)) . i

proof

let i be Nat; :: thesis: (b - 1) / (b to_power (i !)) = ((b - 1) (#) (powerfact b)) . i
((b - 1) (#) (powerfact b)) . i = (b - 1) * ((powerfact b) . i) by VALUED_1:6
.= (b - 1) * (1 / (b to_power (i !))) by DefPower
.= (b - 1) / (b to_power (i !)) by XCMPLX_1:99 ;
hence (b - 1) / (b to_power (i !)) = ((b - 1) (#) (powerfact b)) . i ; :: thesis: verum

end;

A5: for i being Nat holds
( (Liouville_seq (a,b)) . i >= 0 & (Liouville_seq (a,b)) . i <= ((b - 1) (#) (powerfact b)) . i )

proof

let i be Nat; :: thesis: ( (Liouville_seq (a,b)) . i >= 0 & (Liouville_seq (a,b)) . i <= ((b - 1) (#) (powerfact b)) . i )
reconsider b1 = b - 1 as Element of NAT by INT_1:3, XREAL_1:48, A2;

per cases ( i is zero or not i is zero ) ;

suppose A6: i is zero ; :: thesis: ( (Liouville_seq (a,b)) . i >= 0 & (Liouville_seq (a,b)) . i <= ((b - 1) (#) (powerfact b)) . i )

then A7: (Liouville_seq (a,b)) . i = 0 by DefLio;
A8: b to_power (i !) = b by NEWTON:12, A6;
(b - 1) / b >= 0 by A3;
hence ( (Liouville_seq (a,b)) . i >= 0 & (Liouville_seq (a,b)) . i <= ((b - 1) (#) (powerfact b)) . i ) by A7, A4, A8; :: thesis: verum

end;

suppose A9: not i is zero ; :: thesis: ( (Liouville_seq (a,b)) . i >= 0 & (Liouville_seq (a,b)) . i <= ((b - 1) (#) (powerfact b)) . i )

then reconsider ii = i as non zero Nat ;
A10: (Liouville_seq (a,b)) . i = (a . i) / (b to_power (i !)) by A9, DefLio;
reconsider ai = a . i as Nat ;
a . i in rng a by NAT_1:51;
then a . i in b by A1;
then a . i in Segm b by ORDINAL1:def 17;
then ai < b1 + 1 by NAT_1:44;
then ai <= b1 by NAT_1:13;
then (Liouville_seq (a,b)) . i <= (b - 1) / (b to_power (i !)) by A10, XREAL_1:72;
hence ( (Liouville_seq (a,b)) . i >= 0 & (Liouville_seq (a,b)) . i <= ((b - 1) (#) (powerfact b)) . i ) by A4, A10; :: thesis: verum

end;

end;

end;

powerfact b is summable by A2, Th26;
then (b - 1) (#) (powerfact b) is summable by SERIES_1:10;
hence Liouville_seq (a,b) is summable by A5, SERIES_1:20; :: thesis: verum