let m, n be non zero Nat; :: thesis: ( 1 < m implies (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n) )
assume AS: 1 < m ; :: thesis: (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n)
then 1 + 1 <= m by INT_1:7;
then CCM2: ( 2 = m or 2 < m ) by XXREAL_0:1;
reconsider fn = n ! as Real ;
TT1: m to_power n <= m to_power fn by PRE_FF:8, ADDC1, AS;
zz: (Liouville_seq ((seq_const 1),m)) . n = m to_power (- (n !)) by Th39
.= m to_power (- fn)
.= 1 / (m to_power fn) by POWER:28 ;
then ZXC2: (Liouville_seq ((seq_const 1),m)) . n <= 1 / (m to_power n) by TT1, XREAL_1:118;
per cases ( 2 to_power n = m to_power n or 2 to_power n < m to_power n ) by POWER:37, CCM2;
suppose 2 to_power n = m to_power n ; :: thesis: (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n)
hence (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n) by zz, TT1, XREAL_1:118; :: thesis: verum
end;
suppose 2 to_power n < m to_power n ; :: thesis: (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n)
then 1 / (m to_power n) < 1 / (2 to_power n) by XREAL_1:76;
hence (Liouville_seq ((seq_const 1),m)) . n <= 1 / (2 to_power n) by ZXC2, XXREAL_0:2; :: thesis: verum
end;
end;