let a be NAT -valued Real_Sequence; :: thesis: for b, n being Nat st b > 0 holds
(ALiouville_seq (a,b)) . n is Integer
let b, n be Nat; :: thesis: ( b > 0 implies (ALiouville_seq (a,b)) . n is Integer )
set LS = Liouville_seq (a,b);
set BS = BLiouville_seq b;
set AS = ALiouville_seq (a,b);
set ff = ((BLiouville_seq b) . n) (#) ((Liouville_seq (a,b)) |_ (Seg n));
assume A0: b > 0 ; :: thesis: (ALiouville_seq (a,b)) . n is Integer
A1: (ALiouville_seq (a,b)) . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n))) by ALiuDef;
A2: ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n))) = Sum (((BLiouville_seq b) . n) (#) ((Liouville_seq (a,b)) |_ (Seg n))) by SERIES_1:10;
rng (((BLiouville_seq b) . n) (#) ((Liouville_seq (a,b)) |_ (Seg n))) c= INT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (((BLiouville_seq b) . n) (#) ((Liouville_seq (a,b)) |_ (Seg n))) or y in INT )
assume y in rng (((BLiouville_seq b) . n) (#) ((Liouville_seq (a,b)) |_ (Seg n))) ; :: thesis: y in INT
then consider x being object such that
A3: ( x in dom (((BLiouville_seq b) . n) (#) ((Liouville_seq (a,b)) |_ (Seg n))) & y = (((BLiouville_seq b) . n) (#) ((Liouville_seq (a,b)) |_ (Seg n))) . x ) by FUNCT_1:def 3;
reconsider x = x as Nat by A3;
A4: y = ((BLiouville_seq b) . n) * (((Liouville_seq (a,b)) |_ (Seg n)) . x) by A3, VALUED_1:6;
per cases ( x in Seg n or not x in Seg n ) ;
suppose A5: x in Seg n ; :: thesis: y in INT
then A6: ( 1 <= x & x <= n ) by FINSEQ_1:1;
dom (Liouville_seq (a,b)) = NAT by FUNCT_2:def 1;
then x in dom ((Liouville_seq (a,b)) | (Seg n)) by A5, RELAT_1:62;
then A8: ((Liouville_seq (a,b)) |_ (Seg n)) . x = ((Liouville_seq (a,b)) | (Seg n)) . x by FUNCT_4:13
.= (Liouville_seq (a,b)) . x by FUNCT_1:49, A5 ;
((Liouville_seq (a,b)) . x) * ((BLiouville_seq b) . n) is Integer by A0, A6, Th28;
hence y in INT by INT_1:def 2, A4, A8; :: thesis: verum
end;
end;
end;
then reconsider ff = ((BLiouville_seq b) . n) (#) ((Liouville_seq (a,b)) |_ (Seg n)) as INT -valued Real_Sequence by RELAT_1:def 19;
set m = n + 1;
for k being Nat st k >= n + 1 holds
ff . k = 0
proof
let k be Nat; :: thesis: ( k >= n + 1 implies ff . k = 0 )
assume k >= n + 1 ; :: thesis: ff . k = 0
then k > n by NAT_1:13;
then not k in Seg n by FINSEQ_1:1;
then A9: not k in dom ((Liouville_seq (a,b)) | (Seg n)) by RELAT_1:57;
A10: ff . k = ((BLiouville_seq b) . n) * (((Liouville_seq (a,b)) |_ (Seg n)) . k) by VALUED_1:6;
((Liouville_seq (a,b)) |_ (Seg n)) . k = (NAT --> 0) . k by FUNCT_4:11, A9
.= 0 ;
hence ff . k = 0 by A10; :: thesis: verum
end;
hence (ALiouville_seq (a,b)) . n is Integer by A1, A2, Th16; :: thesis: verum