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

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