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

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

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

then HR:
|.(x - (p / q)).| >= 1 / (d * q)
by SS, A1, XREAL_1:72, NAT_1:14;
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 p / q = c / d by XCMPLX_1:94, B1, A1;

hence contradiction by B1, A1; :: thesis: verum

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