let x be Real; :: thesis: ( x is liouville implies x is irrational )
assume A0: x is liouville ; :: thesis: x is irrational
assume x is rational ; :: thesis: contradiction
then consider c being Integer, d being Nat such that
A1: ( d <> 0 & x = c / d ) by RAT_1:8;
consider n being non zero Nat such that
ST: 2 to_power (n - 1) > d by Th10;
consider p being Integer, q being Nat such that
B1: ( q > 1 & 0 < |.(x - (p / q)).| & |.(x - (p / q)).| < 1 / (q |^ n) ) by A0;
SS: |.((c / d) - (p / q)).| = |.(((c * q) - (p * d)) / (d * q)).| by XCMPLX_1:130, B1, A1
.= |.((c * q) - (p * d)).| / |.(d * q).| by COMPLEX1:67
.= |.((c * q) - (p * d)).| / (d * q) ;
(c * q) - (p * d) <> 0
proof
assume (c * q) - (p * d) = 0 ; :: thesis: contradiction
then p / q = c / d by XCMPLX_1:94, B1, A1;
hence contradiction by B1, A1; :: thesis: verum
end;
then HR: |.(x - (p / q)).| >= 1 / (d * q) by SS, A1, XREAL_1:72, NAT_1:14;
d * q < (2 to_power (n - 1)) * q by B1, ST, XREAL_1:68;
then 1 / (d * q) > 1 / ((2 to_power (n - 1)) * q) by XREAL_1:76, A1, B1;
then HG: |.(x - (p / q)).| >= 1 / ((2 to_power (n - 1)) * q) by HR, XXREAL_0:2;
FG: 2 to_power (n - 1) > 0 by POWER:34;
n - 0 >= 1 by NAT_1:14;
then FO: n - 1 >= 0 by XREAL_1:11;
1 + 1 <= q by B1, NAT_1:13;
then 2 to_power (n - 1) <= q to_power (n - 1) by FO, HOLDER_1:3;
then (2 to_power (n - 1)) * q <= (q to_power (n - 1)) * (q to_power 1) by XREAL_1:66, FG;
then (2 to_power (n - 1)) * q <= q to_power ((n - 1) + 1) by B1, POWER:27;
then qa: (2 to_power (n - 1)) * q <= q to_power n ;
2 to_power (n - 1) > 0 by POWER:34;
then 1 / ((2 to_power (n - 1)) * q) >= 1 / (q |^ n) by XREAL_1:118, qa, B1;
hence contradiction by B1, XXREAL_0:2, HG; :: thesis: verum