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

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

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

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

ex i being Nat st
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;((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

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

proof

then consider k being Nat such that
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;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

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