let nl be Liouville; :: thesis: for z being Integer holds z + nl is liouville
let z be Integer; :: thesis: z + nl is liouville
set zl = z + nl;
for n being non zero Nat ex p being Integer ex q being Nat st
( q > 1 & 0 < |.((z + nl) - (p / q)).| & |.((z + nl) - (p / q)).| < 1 / (q |^ n) )

proof

let n be non zero Nat; :: thesis: ex p being Integer ex q being Nat st
( q > 1 & 0 < |.((z + nl) - (p / q)).| & |.((z + nl) - (p / q)).| < 1 / (q |^ n) )
nl is liouville ;
then consider p1 being Integer, q1 being Nat such that
A1: ( q1 > 1 & 0 < |.(nl - (p1 / q1)).| & |.(nl - (p1 / q1)).| < 1 / (q1 |^ n) ) ;
set p2 = (z * q1) + p1;
take (z * q1) + p1 ; :: thesis: ex q being Nat st
( q > 1 & 0 < |.((z + nl) - (((z * q1) + p1) / q)).| & |.((z + nl) - (((z * q1) + p1) / q)).| < 1 / (q |^ n) )
take q2 = q1; :: thesis: ( q2 > 1 & 0 < |.((z + nl) - (((z * q1) + p1) / q2)).| & |.((z + nl) - (((z * q1) + p1) / q2)).| < 1 / (q2 |^ n) )
thus q2 > 1 by A1; :: thesis: ( 0 < |.((z + nl) - (((z * q1) + p1) / q2)).| & |.((z + nl) - (((z * q1) + p1) / q2)).| < 1 / (q2 |^ n) )
((z * q1) + p1) / q2 = ((z * q1) / q1) + (p1 / q1) by XCMPLX_1:62
.= z + (p1 / q1) by A1, XCMPLX_1:89 ;
hence ( 0 < |.((z + nl) - (((z * q1) + p1) / q2)).| & |.((z + nl) - (((z * q1) + p1) / q2)).| < 1 / (q2 |^ n) ) by A1; :: thesis: verum

end;

hence z + nl is liouville by Def2; :: thesis: verum