let r be Real; :: thesis: ( r is liouville iff for n being non zero Nat ex p being Integer ex q being Nat st
( 1 < q & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) ) )
thus ( r is liouville implies for n being non zero Nat ex p being Integer ex q being Nat st
( 1 < q & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) ) ) ; :: thesis: ( ( for n being non zero Nat ex p being Integer ex q being Nat st
( 1 < q & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) ) ) implies r is liouville )
assume Z1: for n being non zero Nat ex p being Integer ex q being Nat st
( 1 < q & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) ) ; :: thesis: r is liouville
let n be Nat; :: according to LIOUVIL1:def 5 :: thesis: ex p being Integer ex q being Nat st
( q > 1 & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) )
per cases ( not n is zero or n is zero ) ;
suppose not n is zero ; :: thesis: ex p being Integer ex q being Nat st
( q > 1 & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) )
hence ex p being Integer ex q being Nat st
( q > 1 & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) ) by Z1; :: thesis: verum
end;
suppose A1: n is zero ; :: thesis: ex p being Integer ex q being Nat st
( q > 1 & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) )
consider p being Integer, q being Nat such that
A2: 1 < q and
A3: 0 < |.(r - (p / q)).| and
A4: |.(r - (p / q)).| < 1 / (q |^ 1) by Z1;
take p ; :: thesis: ex q being Nat st
( q > 1 & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) )
take q ; :: thesis: ( q > 1 & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) )
thus ( 1 < q & 0 < |.(r - (p / q)).| ) by A2, A3; :: thesis: |.(r - (p / q)).| < 1 / (q |^ n)
A5: q |^ 0 = 1 by NEWTON:4;
1 / q < 1 / 1 by A2, XREAL_1:76;
hence |.(r - (p / q)).| < 1 / (q |^ n) by A1, A4, A5, XXREAL_0:2; :: thesis: verum
end;
end;