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
Liouville_constant (a,b) is liouville
let b be non trivial Nat; :: thesis: ( rng a c= b & a is eventually-non-zero implies Liouville_constant (a,b) is liouville )
assume A1: ( rng a c= b & a is eventually-non-zero ) ; :: thesis: Liouville_constant (a,b) is liouville
set x = Liouville_constant (a,b);
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) ) by Th37, A1;
hence Liouville_constant (a,b) is liouville by Def2; :: thesis: verum