:: All Liouville Numbers are Transcendental
:: by Artur Korni{\l}owicz , Adam Naumowicz and Adam Grabowski
::
:: Received February 23, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


set FC = F_Complex ;

set FR = F_Real ;

set Fq = F_Rat ;

set IR = INT.Ring ;

registration
let f be non empty complex-valued Function;
cluster |.f.| -> non empty ;
coherence
not |.f.| is empty
proof end;
end;

theorem Th2: :: LIOUVIL2:1
for m being Nat st 2 <= m holds
for A being Real ex n being positive Nat st A <= m |^ n
proof end;

theorem Th3: :: LIOUVIL2:2
for A being positive Real ex n being positive Nat st 1 / (2 |^ n) <= A
proof end;

registration
let r be Real;
let n be Nat;
cluster K690((r - n),(r + n)) -> right_end ;
coherence
[.(r - n),(r + n).] is right_end
proof end;
end;

registration
let a, b be Real;
cluster K690(a,b) -> closed_interval for Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = [.a,b.] holds
b1 is closed_interval
proof end;
end;

registration
cluster complex V25() ext-real irrational for Element of the carrier of F_Real;
existence
ex b1 being Element of F_Real st b1 is irrational
proof end;
end;

theorem Th4: :: LIOUVIL2:3
F_Real is Subring of F_Complex by RING_3:43, RING_3:48;

theorem Th5: :: LIOUVIL2:4
F_Rat is Subring of F_Real by GAUSSINT:14, RING_3:43;

theorem :: LIOUVIL2:5
INT.Ring is Subring of F_Real by Th5, RING_3:47, ALGNUM_1:1;

theorem Th7: :: LIOUVIL2:6
for R being Ring
for S being Subring of R
for x being Element of S holds x is Element of R
proof end;

theorem Th8: :: LIOUVIL2:7
for R being Ring
for S being Subring of R
for f being Polynomial of S holds f is Polynomial of R
proof end;

theorem Th9: :: LIOUVIL2:8
for R being Ring
for S being Subring of R
for f being Polynomial of S
for g being Polynomial of R st f = g holds
len f = len g
proof end;

theorem :: LIOUVIL2:9
for R being Ring
for S being Subring of R
for f being Polynomial of S
for g being Polynomial of R st f = g holds
LC f = LC g by Th9;

theorem :: LIOUVIL2:10
for R being non degenerated Ring
for S being Subring of R
for f being Polynomial of S
for g being monic Polynomial of R st f = g holds
f is monic
proof end;

registration
let R be non degenerated Ring;
cluster -> non degenerated for Subring of R;
coherence
for b1 being Subring of R holds not b1 is degenerated
proof end;
cluster non empty non degenerated left_add-cancelable right_add-cancelable right_complementable V101() V102() V103() right-distributive left-distributive right_unital well-unital V123() left_unital unital V134() V315() V316() V317() V318() for Subring of R;
existence
not for b1 being Subring of R holds b1 is degenerated
proof end;
end;

theorem :: LIOUVIL2:11
for R being non degenerated Ring
for S being non degenerated Subring of R
for f being monic Polynomial of S
for g being Polynomial of R st f = g holds
g is monic
proof end;

theorem Th13: :: LIOUVIL2:12
for R being non degenerated Ring
for S being Subring of R
for f being Polynomial of S
for g being non-zero Polynomial of R st f = g holds
f is non-zero
proof end;

theorem :: LIOUVIL2:13
for R being non degenerated Ring
for S being Subring of R
for f being non-zero Polynomial of S
for g being Polynomial of R st f = g holds
g is non-zero
proof end;

theorem Th15: :: LIOUVIL2:14
for R, T being Ring
for S being Subring of R
for f being Polynomial of S
for g being Polynomial of R st f = g holds
for a being Element of R holds Ext_eval (f,(In (a,T))) = Ext_eval (g,(In (a,T)))
proof end;

theorem Th16: :: LIOUVIL2:15
for R being Ring
for S being Subring of R
for f being Polynomial of S
for r being Element of R
for s being Element of S st r = s holds
Ext_eval (f,r) = Ext_eval (f,s)
proof end;

theorem :: LIOUVIL2:16
for R being Ring
for S being Subring of R
for r being Element of R
for s being Element of S st r = s & s is_integral_over S holds
r is_integral_over R
proof end;

theorem Th18: :: LIOUVIL2:17
for R being Ring
for S being Subring of R
for r being Element of R
for s being Element of S
for f being Polynomial of R
for g being Polynomial of S st r = s & f = g & r is_a_root_of f holds
s is_a_root_of g
proof end;

theorem Th19: :: LIOUVIL2:18
for R being Ring holds R is Subring of R
proof end;

Lm1: 0. F_Complex = 0
by COMPLFLD:def 1;

Lm2: 1. F_Complex = 1
by COMPLFLD:def 1;

Lm3: F_Complex is Subring of F_Complex
by Th19;

registration
cluster 0_. F_Complex -> INT -valued ;
coherence
0_. F_Complex is INT -valued by Lm1;
cluster 1_. F_Complex -> INT -valued ;
coherence
1_. F_Complex is INT -valued
proof end;
end;

registration
let L be non empty non degenerated doubleLoopStr ;
cluster Function-like V44( NAT , the carrier of L) finite-Support monic -> non-zero for Element of K19(K20(NAT, the carrier of L));
coherence
for b1 being Polynomial of L st b1 is monic holds
b1 is non-zero ;
end;

registration
cluster Relation-like NAT -defined INT -valued the carrier of F_Complex -valued Function-like V44( NAT , the carrier of F_Complex) complex-valued finite-Support monic for Element of K19(K20(NAT, the carrier of F_Complex));
existence
ex b1 being Polynomial of F_Complex st
( b1 is monic & b1 is INT -valued )
proof end;
cluster Relation-like NAT -defined RAT -valued the carrier of F_Complex -valued Function-like V44( NAT , the carrier of F_Complex) complex-valued finite-Support monic for Element of K19(K20(NAT, the carrier of F_Complex));
existence
ex b1 being Polynomial of F_Complex st
( b1 is monic & b1 is RAT -valued )
proof end;
cluster Relation-like NAT -defined REAL -valued the carrier of F_Complex -valued Function-like V44( NAT , the carrier of F_Complex) complex-valued finite-Support monic for Element of K19(K20(NAT, the carrier of F_Complex));
existence
ex b1 being Polynomial of F_Complex st
( b1 is monic & b1 is REAL -valued )
proof end;
end;

theorem Th20: :: LIOUVIL2:19
for f being INT -valued Polynomial of F_Complex holds f is Polynomial of INT.Ring
proof end;

theorem Th21: :: LIOUVIL2:20
for f being RAT -valued Polynomial of F_Complex holds f is Polynomial of F_Rat
proof end;

theorem Th22: :: LIOUVIL2:21
for f being REAL -valued Polynomial of F_Complex holds f is Polynomial of F_Real
proof end;

registration
let L be non empty ZeroStr ;
cluster Function-like V44( NAT , the carrier of L) finite-Support non-zero -> non zero for Element of K19(K20(NAT, the carrier of L));
correctness
coherence
for b1 being Polynomial of L st b1 is non-zero holds
not b1 is zero ;
;
cluster Function-like V44( NAT , the carrier of L) finite-Support zero -> non non-zero for Element of K19(K20(NAT, the carrier of L));
correctness
coherence
for b1 being Polynomial of L st b1 is zero holds
not b1 is non-zero ;
;
end;

theorem Th23: :: LIOUVIL2:22
for i being Integer
for f being INT -valued FinSequence st i in rng f holds
i divides Product f
proof end;

theorem Th24: :: LIOUVIL2:23
for c being Element of F_Complex holds
( ex f being INT -valued non-zero Polynomial of F_Complex st c is_a_root_of f iff ex f being RAT -valued monic Polynomial of F_Complex st c is_a_root_of f )
proof end;

theorem Th25: :: LIOUVIL2:24
for c being Element of F_Complex holds
( c is algebraic iff ex f being RAT -valued monic Polynomial of F_Complex st c is_a_root_of f )
proof end;

theorem Th26: :: LIOUVIL2:25
for c being Element of F_Complex holds
( c is algebraic iff ex f being INT -valued non-zero Polynomial of F_Complex st c is_a_root_of f )
proof end;

theorem Th27: :: LIOUVIL2:26
for c being Element of F_Complex holds
( c is algebraic_integer iff ex f being INT -valued monic Polynomial of F_Complex st c is_a_root_of f )
proof end;

registration
cluster complex algebraic_integer -> algebraic for object ;
coherence
for b1 being Complex st b1 is algebraic_integer holds
b1 is algebraic
proof end;
cluster complex transcendental -> non algebraic_integer for object ;
coherence
for b1 being Complex st b1 is transcendental holds
not b1 is algebraic_integer ;
end;

:: WP: Liouville's theorem on diophantine approximation
theorem Th28: :: LIOUVIL2:27
for f being INT -valued non-zero Polynomial of F_Real
for a being irrational Element of F_Real st a is_a_root_of f holds
ex A being positive Real st
for p being Integer
for q being positive Nat holds |.(a - (p / q)).| > A / (q |^ (len f))
proof end;

Lm4: now :: thesis: for n being Nat
for L being Liouville
for A being positive Real holds
not for p being Integer
for q being positive Nat holds |.(L - (p / q)).| > A / (q |^ n)
let n be Nat; :: thesis: for L being Liouville
for A being positive Real holds
not for p being Integer
for q being positive Nat holds |.(L - (p / q)).| > A / (q |^ n)
let L be Liouville; :: thesis: for A being positive Real holds
not for p being Integer
for q being positive Nat holds |.(L - (p / q)).| > A / (q |^ n)
let A be positive Real; :: thesis: not for p being Integer
for q being positive Nat holds |.(L - (p / q)).| > A / (q |^ n)
assume A1: for p being Integer
for q being positive Nat holds |.(L - (p / q)).| > A / (q |^ n) ; :: thesis: contradiction
consider r being positive Nat such that
A2: 1 / (2 |^ r) <= A by Th3;
consider p being Integer, q being Nat such that
A3: 1 < q and
0 < |.(L - (p / q)).| and
A4: |.(L - (p / q)).| < 1 / (q |^ (r + n)) by LIOUVIL1:def 5;
A5: q |^ (r + n) = (q |^ r) * (q |^ n) by NEWTON:8;
1 + 1 <= q by A3, NAT_1:13;
then 2 |^ r <= q |^ r by PREPOWER:9;
then A6: 1 / (2 |^ r) >= 1 / (q |^ r) by XREAL_1:118;
1 / ((q |^ r) * (q |^ n)) = (1 / (q |^ r)) * (1 / (q |^ n)) by XCMPLX_1:102;
then A7: 1 / ((q |^ r) * (q |^ n)) <= (1 / (2 |^ r)) * (1 / (q |^ n)) by A6, XREAL_1:64;
(1 / (2 |^ r)) * (1 / (q |^ n)) <= A * (1 / (q |^ n)) by A2, XREAL_1:64;
then 1 / ((q |^ r) * (q |^ n)) <= A / (q |^ n) by A7, XXREAL_0:2;
hence contradiction by A1, A3, A4, A5, XXREAL_0:2; :: thesis: verum
end;

:: WP: All Liouville numbers are transcendental
registration
cluster V25() liouville -> transcendental for object ;
coherence
for b1 being Liouville holds b1 is transcendental
proof end;
end;