let a be NAT -valued Real_Sequence; :: thesis: for b, n, k being Nat st b > 0 & k <= n holds
((Liouville_seq (a,b)) . k) * ((BLiouville_seq b) . n) is Integer
let b, n, k be Nat; :: thesis: ( b > 0 & k <= n implies ((Liouville_seq (a,b)) . k) * ((BLiouville_seq b) . n) is Integer )
assume A1: ( b > 0 & k <= n ) ; :: thesis: ((Liouville_seq (a,b)) . k) * ((BLiouville_seq b) . n) is Integer
then 0 + (k !) <= n ! by SIN_COS:39;
then A2: (n !) - (k !) in NAT by INT_1:3, XREAL_1:19;
set bk = b to_power (k !);
set bn = b to_power (n !);
A3: (b to_power (n !)) / (b to_power (k !)) = b to_power ((n !) - (k !)) by A1, POWER:29;

per cases ( k = 0 or not k is zero ) ;

suppose k = 0 ; :: thesis: ((Liouville_seq (a,b)) . k) * ((BLiouville_seq b) . n) is Integer

then (Liouville_seq (a,b)) . k = 0 by DefLio;
hence ((Liouville_seq (a,b)) . k) * ((BLiouville_seq b) . n) is Integer ; :: thesis: verum

end;

suppose not k is zero ; :: thesis: ((Liouville_seq (a,b)) . k) * ((BLiouville_seq b) . n) is Integer

then (Liouville_seq (a,b)) . k = (a . k) / (b to_power (k !)) by DefLio;
then ((Liouville_seq (a,b)) . k) * ((BLiouville_seq b) . n) = ((a . k) / (b to_power (k !))) * ((b to_power (n !)) / 1) by LiuSeq
.= ((a . k) * (b to_power (n !))) / ((b to_power (k !)) * 1) by XCMPLX_1:76
.= (a . k) * ((b to_power (n !)) / (b to_power (k !))) by XCMPLX_1:74 ;
hence ((Liouville_seq (a,b)) . k) * ((BLiouville_seq b) . n) is Integer by A2, A3; :: thesis: verum

end;

end;