let a be NAT -valued Real_Sequence; :: thesis: for b, c being Nat st b >= 2 & c >= 1 & rng a c= c & c <= b holds
for i being Nat holds (Liouville_seq (a,b)) . i <= ((c - 1) (#) (powerfact b)) . i
let b, c be Nat; :: thesis: ( b >= 2 & c >= 1 & rng a c= c & c <= b implies for i being Nat holds (Liouville_seq (a,b)) . i <= ((c - 1) (#) (powerfact b)) . i )
assume A1: ( b >= 2 & c >= 1 & rng a c= c & c <= b ) ; :: thesis: for i being Nat holds (Liouville_seq (a,b)) . i <= ((c - 1) (#) (powerfact b)) . i
set f = Liouville_seq (a,b);
A2: for i being Nat holds (c - 1) / (b to_power (i !)) = ((c - 1) (#) (powerfact b)) . i

proof

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

end;

let i be Nat; :: thesis: (Liouville_seq (a,b)) . i <= ((c - 1) (#) (powerfact b)) . i
A4: b >= 1 by A1, XXREAL_0:2;
reconsider b1 = b - 1 as Element of NAT by A4, INT_1:3, XREAL_1:48;
reconsider c1 = c - 1 as Element of NAT by A1, INT_1:3, XREAL_1:48;

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

suppose A5: i is zero ; :: thesis: (Liouville_seq (a,b)) . i <= ((c - 1) (#) (powerfact b)) . i

then A6: (Liouville_seq (a,b)) . i = 0 by DefLio;
A7: b to_power (i !) = b by NEWTON:12, A5;
c1 >= 0 ;
then (c - 1) / b >= 0 ;
hence (Liouville_seq (a,b)) . i <= ((c - 1) (#) (powerfact b)) . i by A2, A6, A7; :: thesis: verum

end;

suppose A8: not i is zero ; :: thesis: (Liouville_seq (a,b)) . i <= ((c - 1) (#) (powerfact b)) . i

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

end;

end;