:: by Artur Korni{\l}owicz , Adam Naumowicz and Adam Grabowski

::

:: Received February 23, 2017

:: 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
end;

registration

let a, b be Real;

coherence

for b_{1} being Subset of REAL st b_{1} = [.a,b.] holds

b_{1} is closed_interval

end;
coherence

for b

b

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

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;

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

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;

coherence

for b_{1} being Subring of R holds not b_{1} is degenerated

not for b_{1} being Subring of R holds b_{1} is degenerated

end;
coherence

for b

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() V313() V314() V315() V316() for Subring of R;

existence not for b

proof 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

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

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

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

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)

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

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

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;

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

registration

let L be non empty non degenerated doubleLoopStr ;

for b_{1} being Polynomial of L st b_{1} is monic holds

b_{1} is non-zero
;

end;
cluster Function-like V44( NAT , the carrier of L) finite-Support monic -> non-zero for Polynomial of ;

coherence for b

b

registration

ex b_{1} being Polynomial of F_Complex st

( b_{1} is monic & b_{1} is INT -valued )

ex b_{1} being Polynomial of F_Complex st

( b_{1} is monic & b_{1} is RAT -valued )

ex b_{1} being Polynomial of F_Complex st

( b_{1} is monic & b_{1} is REAL -valued )
end;

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 Polynomial of ;

existence ex b

( b

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 Polynomial of ;

existence ex b

( b

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 Polynomial of ;

existence ex b

( b

proof end;

registration

let L be non empty ZeroStr ;

coherence

for b_{1} being Polynomial of L st b_{1} is non-zero holds

not b_{1} is zero ;

;

coherence

for b_{1} being Polynomial of L st b_{1} is zero holds

not b_{1} is non-zero ;

;

end;
cluster Function-like V44( NAT , the carrier of L) finite-Support non-zero -> non zero for Polynomial of ;

correctness coherence

for b

not b

;

cluster Function-like V44( NAT , the carrier of L) finite-Support zero -> non non-zero for Polynomial of ;

correctness coherence

for b

not b

;

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 )

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

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

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

( 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 b_{1} being Complex st b_{1} is algebraic_integer holds

b_{1} is algebraic

for b_{1} being Complex st b_{1} is transcendental holds

not b_{1} is algebraic_integer
;

end;
for b

b

proof end;

coherence for b

not b

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

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)

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