:: All Liouville Numbers are Transcendental
::
:: Copyright (c) 2017-2018 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 K687((r - n),(r + n)) -> right_end ;
coherence
[.(r - n),(r + n).] is right_end
proof end;
end;

registration
let a, b be Real;
cluster K687(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
existence
ex b1 being Element of F_Real st b1 is irrational
proof end;
end;

theorem Th4: :: LIOUVIL2:3

theorem Th5: :: LIOUVIL2:4

theorem :: LIOUVIL2:5
INT.Ring is Subring of F_Real by ;

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;
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:
by COMPLFLD:def 1;

Lm2:
by COMPLFLD:def 1;

Lm3:
by Th19;

registration
coherence by Lm1;
coherence
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 Polynomial of ;
coherence
for b1 being Polynomial of L st b1 is monic holds
b1 is non-zero
;
end;

registration
existence
ex b1 being Polynomial of F_Complex st
( b1 is monic & b1 is INT -valued )
proof end;
existence
ex b1 being Polynomial of F_Complex st
( b1 is monic & b1 is RAT -valued )
proof end;
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 Polynomial of ;
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 Polynomial of ;
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
coherence
for b1 being Complex st b1 is algebraic_integer holds
b1 is algebraic
proof end;
coherence
for b1 being Complex st b1 is transcendental holds
not b1 is algebraic_integer
;
end;

:: 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 ;
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 ;
(1 / (2 |^ r)) * (1 / (q |^ n)) <= A * (1 / (q |^ n)) by ;
then 1 / ((q |^ r) * (q |^ n)) <= A / (q |^ n) by ;
hence contradiction by ; :: thesis: verum
end;

:: All Liouville numbers are transcendental
registration
coherence
for b1 being Liouville holds b1 is transcendental
proof end;
end;