let a be NAT -valued Real_Sequence; :: thesis: for b being non trivial Nat st rng a c= b & a is eventually-non-zero holds
for n being non zero Nat ex p being Integer ex q being Nat st
( q > 1 & 0 < |.((Liouville_constant (a,b)) - (p / q)).| & |.((Liouville_constant (a,b)) - (p / q)).| < 1 / (q |^ n) )
let b be non trivial Nat; :: thesis: ( rng a c= b & a is eventually-non-zero implies for n being non zero Nat ex p being Integer ex q being Nat st
( q > 1 & 0 < |.((Liouville_constant (a,b)) - (p / q)).| & |.((Liouville_constant (a,b)) - (p / q)).| < 1 / (q |^ n) ) )
assume A1: ( rng a c= b & a is eventually-non-zero ) ; :: thesis: for n being non zero Nat ex p being Integer ex q being Nat st
( q > 1 & 0 < |.((Liouville_constant (a,b)) - (p / q)).| & |.((Liouville_constant (a,b)) - (p / q)).| < 1 / (q |^ n) )
set x = Liouville_constant (a,b);
A2: b >= 1 + 1 by NAT_2:29;
then A3: b > 1 by NAT_1:13;
set pn = ALiouville_seq (a,b);
set qn = BLiouville_seq b;
let n be non zero Nat; :: thesis: ex p being Integer ex q being Nat st
( q > 1 & 0 < |.((Liouville_constant (a,b)) - (p / q)).| & |.((Liouville_constant (a,b)) - (p / q)).| < 1 / (q |^ n) )
A4: n >= 0 + 1 by NAT_1:13;
reconsider p = (ALiouville_seq (a,b)) . n as Integer ;
reconsider q = (BLiouville_seq b) . n as Nat ;
take p ; :: thesis: ex q being Nat st
( q > 1 & 0 < |.((Liouville_constant (a,b)) - (p / q)).| & |.((Liouville_constant (a,b)) - (p / q)).| < 1 / (q |^ n) )
take q ; :: thesis: ( q > 1 & 0 < |.((Liouville_constant (a,b)) - (p / q)).| & |.((Liouville_constant (a,b)) - (p / q)).| < 1 / (q |^ n) )
A5: q = b to_power (n !) by LiuSeq;
thus q > 1 by Th30, A3; :: thesis: ( 0 < |.((Liouville_constant (a,b)) - (p / q)).| & |.((Liouville_constant (a,b)) - (p / q)).| < 1 / (q |^ n) )
set LS = Liouville_seq (a,b);
A6: Liouville_seq (a,b) is summable by Th31, NAT_2:29, A1;
A7: Sum ((Liouville_seq (a,b)) ^\ (n + 1)) > 0 by Th36, A1;
(Liouville_seq (a,b)) . 0 = 0 by DefLio;
then A8: Sum (Liouville_seq (a,b)) = (Sum (FinSeq ((Liouville_seq (a,b)),n))) + (Sum ((Liouville_seq (a,b)) ^\ (n + 1))) by Th23, A6;
A9: |.((Liouville_constant (a,b)) - (p / q)).| = |.((Sum (Liouville_seq (a,b))) - (Sum (FinSeq ((Liouville_seq (a,b)),n)))).| by A3, Th32
.= Sum ((Liouville_seq (a,b)) ^\ (n + 1)) by A7, A8, ABSVALUE:def 1 ;
A10: Sum ((Liouville_seq (a,b)) ^\ (n + 1)) <= Sum ((b - 1) (#) ((powerfact b) ^\ (n + 1))) by A1, A2, A3, Th35;
Sum ((b - 1) (#) ((powerfact b) ^\ (n + 1))) < 1 / ((b to_power (n !)) to_power n) by A3, A4, Th27;
hence ( 0 < |.((Liouville_constant (a,b)) - (p / q)).| & |.((Liouville_constant (a,b)) - (p / q)).| < 1 / (q |^ n) ) by A1, A5, A9, A10, XXREAL_0:2, Th36; :: thesis: verum