let a be NAT -valued Real_Sequence; :: thesis: for b being non trivial Nat
for n being Nat st a is eventually-non-zero & rng a c= b holds
Sum ((Liouville_seq (a,b)) ^\ (n + 1)) > 0
let b be non trivial Nat; :: thesis: for n being Nat st a is eventually-non-zero & rng a c= b holds
Sum ((Liouville_seq (a,b)) ^\ (n + 1)) > 0
let n be Nat; :: thesis: ( a is eventually-non-zero & rng a c= b implies Sum ((Liouville_seq (a,b)) ^\ (n + 1)) > 0 )
assume A1: ( a is eventually-non-zero & rng a c= b ) ; :: thesis: Sum ((Liouville_seq (a,b)) ^\ (n + 1)) > 0
set LS = (Liouville_seq (a,b)) ^\ (n + 1);
A2: 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
((Liouville_seq (a,b)) ^\ (n + 1)) . i = (Liouville_seq (a,b)) . ((n + 1) + i) by NAT_1:def 3;
hence 0 <= ((Liouville_seq (a,b)) ^\ (n + 1)) . i by Th33; :: thesis: verum

end;

ex i being Nat st
( i in dom ((Liouville_seq (a,b)) ^\ (n + 1)) & 0 < ((Liouville_seq (a,b)) ^\ (n + 1)) . i )

proof

consider j being Nat such that
A3: ( n + 1 <= j & a . j <> 0 ) by A1;
j - (n + 1) in NAT by A3, INT_1:5;
then reconsider i = j - (n + 1) as Nat ;
take i ; :: thesis: ( i in dom ((Liouville_seq (a,b)) ^\ (n + 1)) & 0 < ((Liouville_seq (a,b)) ^\ (n + 1)) . i )
A4: (n + 1) + i = j ;
A5: dom ((Liouville_seq (a,b)) ^\ (n + 1)) = NAT by FUNCT_2:def 1;
((Liouville_seq (a,b)) ^\ (n + 1)) . i = (Liouville_seq (a,b)) . j by NAT_1:def 3, A4
.= (a . ((n + 1) + i)) / (b to_power (j !)) by DefLio ;
hence ( i in dom ((Liouville_seq (a,b)) ^\ (n + 1)) & 0 < ((Liouville_seq (a,b)) ^\ (n + 1)) . i ) by A5, A3, ORDINAL1:def 12; :: thesis: verum

end;

then consider k being Nat such that
A6: ( k in dom ((Liouville_seq (a,b)) ^\ (n + 1)) & ((Liouville_seq (a,b)) ^\ (n + 1)) . k > 0 ) ;
Liouville_seq (a,b) is summable by Th31, A1, NAT_2:29;
then (Liouville_seq (a,b)) ^\ (n + 1) is summable by SERIES_1:12;
hence Sum ((Liouville_seq (a,b)) ^\ (n + 1)) > 0 by A6, RSSPACE2:3, A2; :: thesis: verum