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) )

( 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 )
;

end;

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) )

( 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;( q > 1 & 0 < |.(r - (p / q)).| & |.(r - (p / q)).| < 1 / (q |^ n) ) by Z1; :: thesis: verum

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) )

( 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;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