:: All Liouville Numbers are Transcendental
:: by Artur Korni{\l}owicz , Adam Naumowicz and Adam Grabowski
::
:: Received February 23, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, CARD_1, ARYTM_1, TARSKI, ARYTM_3, REAL_1,
NAT_1, INT_1, XCMPLX_0, LIOUVIL1, COMPLEX1, NEWTON, IRRAT_1, FUNCT_7,
FINSET_1, FUNCT_1, CARD_3, ALGNUM_1, COMPLFLD, XBOOLE_0, POLYNOM1,
RELAT_1, VECTSP_1, POLYNOM5, XXREAL_0, FINSEQ_1, GAUSSINT, RATFUNC1,
MESFUNC1, SUPINF_2, POLYNOM2, C0SP1, FUNCSDOM, STRUCT_0, POLYNOM3,
VALUED_0, INT_3, ALGSEQ_1, GROUP_1, PARTFUN1, CAT_1, ALGSTR_0, MSAFREE2,
XXREAL_1, ORDINAL2, XXREAL_2, FDIFF_1, MEASURE5, ORDINAL4, FINSEQ_2,
BINOP_2, SETWISEO, WAYBEL_8;
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1,
PARTFUN1, FINSEQ_1, NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, NAT_1, NAT_D,
FINSEQ_2, BINOP_2, SETWOP_2, XXREAL_0, XXREAL_2, RCOMP_1, VALUED_0,
VALUED_1, INT_1, NEWTON, RAT_1, COMSEQ_2, MEASURE5, IRRAT_1, FCONT_1,
FDIFF_1, RVSUM_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_4, VECTSP_1, C0SP1,
INT_3, COMPLFLD, GAUSSINT, ALGSEQ_1, POLYNOM3, POLYNOM4, POLYNOM5,
UPROOTS, RATFUNC1, RING_4, ALGNUM_1, POLYDIFF, FVSUM_1, LIOUVIL1;
constructors NEWTON, ALGNUM_1, ALGSEQ_1, C0SP1, POLYNOM4, FUNCT_7, TOPMETR,
EC_PF_1, BINOP_2, NAT_D, RATFUNC1, RCOMP_1, UPROOTS, GR_CY_1, FVSUM_1,
GAUSSINT, REALSET1, POLYDIFF, XXREAL_2, FCONT_1, MEASURE5, COMSEQ_2,
GROUP_4, FINSOP_1, ALGSTR_1, LIOUVIL1;
registrations XREAL_0, RELAT_1, ORDINAL1, RAT_1, INT_1, XXREAL_0, INT_6,
VECTSP_1, POLYNOM3, STRUCT_0, MEMBERED, RELSET_1, POLYNOM5, RING_4,
XCMPLX_0, NUMBERS, XBOOLE_0, NAT_1, VALUED_0, RATFUNC1, FINSEQ_1, NEWTON,
FINSEQ_2, WSIERP_1, ABSVALUE, NIVEN, COMPLFLD, ALGSTR_1, POLYNOM4,
GAUSSINT, INT_3, SUBSET_1, NEWTON04, UPROOTS, POLYDIFF, XXREAL_1,
XXREAL_2, FINSET_1, FCONT_1, COMPLEX1, RCOMP_1, IDEAL_1, RFUNCT_1,
PREPOWER, LIOUVIL1, ALGNUM_1, INT_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RELAT_1, STRUCT_0, ALGSEQ_1, C0SP1, POLYNOM5, RATFUNC1,
ALGNUM_1, MEASURE5;
equalities STRUCT_0, VECTSP_1, GAUSSINT, RATFUNC1, POLYNOM3, INT_3, COMPLEX1,
REALSET1, POLYDIFF, XCMPLX_0;
expansions TARSKI, ALGNUM_1, UPROOTS, ALGSEQ_1, RATFUNC1, POLYNOM5, FDIFF_1,
INT_1;
theorems XREAL_0, NEWTON, XXREAL_0, XREAL_1, XCMPLX_1, NAT_1, PREPOWER,
ALGNUM_1, COMPLFLD, RING_3, POLYNOM4, UPROOTS, INT_1, GAUSSINT, C0SP1,
FUNCT_2, ALGSEQ_1, RLVECT_1, FINSEQ_3, FINSEQ_2, ZFMISC_1, FUNCT_7,
RATFUNC1, RELAT_1, FINSEQ_1, FUNCT_1, POLYDIFF, XXREAL_2, ROLLE,
COMPLEX1, POLYNOM5, XXREAL_1, XBOOLE_0, TARSKI, FDIFF_1, ABSVALUE,
VALUED_1, INTEGRA5, INTEGRA1, RAT_1, NAT_3, FVSUM_1, NIVEN, NAT_D,
RVSUM_1, INT_2, XCMPLX_0, NUMBERS, RING_2, GROUP_4, LIOUVIL1;
schemes FRAENKEL, FINSEQ_1, FINSEQ_2, POLYNOM3;
begin
reserve m,n for Nat;
reserve r for Real;
reserve c for Element of F_Complex;
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
proof
dom |.f.| = dom f by VALUED_1:def 11;
hence thesis;
end;
end;
theorem Th2:
2 <= m implies for A being Real
ex n being positive Nat st A <= m|^n
proof
assume 2 <= m; then 1 + 1 <= m;
then
A1: 1 < m by NAT_1:13;
let A be Real;
reconsider a=|.[/ A \].| as Nat by TARSKI:1;
reconsider n=a+1 as positive Nat;
A <= [/A\] & [/ A \] <= a by ABSVALUE:4,INT_1:def 7;
then A2: A <= a by XXREAL_0:2;
a < n & n <= m |^ n by A1,NAT_3:2,NAT_1:13;
then a <= m |^ n by XXREAL_0:2;
hence thesis by A2,XXREAL_0:2;
end;
theorem Th3:
for A being positive Real
ex n being positive Nat st 1/(2|^n) <= A
proof
let A be positive Real;
consider n being positive Nat such that
A1: 1/A <= 2|^n by Th2;
take n;
1/(1/A) >= 1/(2|^n) by A1,XREAL_1:118;
hence thesis;
end;
registration
let r,n;
cluster [.r-n,r+n.] -> right_end;
coherence
proof
r-n <= r+n by XREAL_1:6;
hence thesis by XXREAL_2:33;
end;
end;
registration
let a,b be Real;
cluster [.a,b.] -> closed_interval for Subset of REAL;
coherence
proof
let X be Subset of REAL;
assume X = [.a,b.];
hence ex x,y being Real st X = [.x,y.];
end;
end;
registration
cluster irrational for Element of F_Real;
existence
proof
reconsider a = the irrational Real as Element of FR by XREAL_0:def 1;
take a;
thus thesis;
end;
end;
theorem Th4:
F_Real is Subring of F_Complex by RING_3:43,48;
theorem Th5:
F_Rat is Subring of F_Real by GAUSSINT:14,RING_3:43;
theorem
INT.Ring is Subring of F_Real by Th5,RING_3:47,ALGNUM_1:1;
theorem Th7:
for R being Ring, S being Subring of R
for x being Element of S holds x is Element of R
proof
let R be Ring;
let S be Subring of R;
let x be Element of S;
the carrier of S c= the carrier of R by C0SP1:def 3;
hence x is Element of R;
end;
theorem Th8:
for R being Ring, S being Subring of R
for f being Polynomial of S holds
f is Polynomial of R
proof
let R be Ring, S be Subring of R;
let f be Polynomial of S;
the carrier of S c= the carrier of R by C0SP1:def 3;
then reconsider f as sequence of R by FUNCT_2:7;
f is finite-Support
proof
consider n such that
A1: for i being Nat st i >= n holds f.i = 0.S by ALGSEQ_1:def 1;
take n;
0.S = 0.R by C0SP1:def 3;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th9:
for R being Ring, 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
let R be Ring;
let S be Subring of R;
let f be Polynomial of S;
let g be Polynomial of R;
assume
A1: f = g;
A2: len g is_at_least_length_of f
proof
let i be Nat;
assume i >= len g;
then g.i = 0.R by ALGSEQ_1:8;
hence f.i = 0.S by A1,C0SP1:def 3;
end;
for m being Nat st m is_at_least_length_of f holds len g <= m
proof
let m be Nat;
assume
A3: m is_at_least_length_of f;
m is_at_least_length_of g
proof
let i be Nat;
assume i >= m;
then f.i = 0.S by A3;
hence g.i = 0.R by A1,C0SP1:def 3;
end;
hence len g <= m by ALGSEQ_1:def 3;
end;
hence thesis by A2,ALGSEQ_1:def 3;
end;
theorem
for R being Ring, 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
for R being non degenerated Ring, 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
let R be non degenerated Ring;
let S be Subring of R;
let f be Polynomial of S;
let g be monic Polynomial of R;
assume f = g;
hence LC f = LC g by Th9
.= 1.R by RATFUNC1:def 7
.= 1.S by C0SP1:def 3;
end;
registration
let R be non degenerated Ring;
cluster -> non degenerated for Subring of R;
coherence
proof
let S be Subring of R;
0.S = 0.R & 1.S = 1.R by C0SP1:def 3;
hence 0.S <> 1.S;
end;
cluster non degenerated for Subring of R;
existence
proof
take the Subring of R;
thus thesis;
end;
end;
theorem
for R being non degenerated Ring, 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
let R be non degenerated Ring;
let S be non degenerated Subring of R;
let f be monic Polynomial of S;
let g be Polynomial of R;
assume f = g;
hence LC g = LC f by Th9
.= 1.S by RATFUNC1:def 7
.= 1.R by C0SP1:def 3;
end;
theorem Th13:
for R being non degenerated Ring, 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
let R be non degenerated Ring;
let S be Subring of R;
let f be Polynomial of S;
let g be non-zero Polynomial of R;
assume f = g;
then
A1: len f = len g by Th9;
0 < len g by UPROOTS:17;
hence thesis by A1,UPROOTS:17;
end;
theorem
for R being non degenerated Ring, 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
let R be non degenerated Ring;
let S be Subring of R;
let f be non-zero Polynomial of S;
let g be Polynomial of R;
assume f = g;
then
A1: len f = len g by Th9;
0 < len f by UPROOTS:17;
hence thesis by A1,UPROOTS:17;
end;
theorem Th15:
for R,T being Ring, S being Subring of R
for f being Polynomial of S
for g being Polynomial of R st f = g
for a being Element of R
holds Ext_eval(f,In(a,T)) = Ext_eval(g,In(a,T))
proof
let R,T be Ring;
let S be Subring of R;
let f be Polynomial of S;
let g be Polynomial of R;
assume
A1: f = g;
let a be Element of R;
consider F being FinSequence of T such that
A2: Ext_eval(f,In(a,T)) = Sum F and
A3: len F = len f and
A4: for n being Element of NAT st n in dom F holds
F.n = In(f.(n-'1),T) * (power T).(In(a,T),n-'1) by ALGNUM_1:def 1;
consider G being FinSequence of T such that
A5: Ext_eval(g,In(a,T)) = Sum G and
A6: len G = len g and
A7: for n being Element of NAT st n in dom G holds
G.n = In(g.(n-'1),T) * (power T).(In(a,T),n-'1) by ALGNUM_1:def 1;
consider Z being sequence of T such that
A8: Sum G = Z.(len G) and
A9: Z.0 = 0.T and
A10: for j being Nat, v being Element of T st j < len G & v = G.(j+1)
holds Z.(j+1) = Z.j + v by RLVECT_1:def 12;
A11: Sum G = Z.(len F) by A1,A3,A6,A8,Th9;
now
let j be Nat, v be Element of T such that
A12: j < len F and
A13: v = F.(j+1);
A14: len F = len G by A1,A3,A6,Th9;
A15: dom F = dom G by A1,A3,A6,Th9,FINSEQ_3:29;
j+1 <= len F by A12,NAT_1:13;
then
A16: j+1 in dom F by NAT_1:11,FINSEQ_3:25;
then F.(j+1) = In(f.(j+1-'1),T) * (power T).(In(a,T),j+1-'1) by A4
.= G.(j+1) by A1,A7,A15,A16;
hence Z.(j+1) = Z.j + v by A10,A12,A13,A14;
end;
hence thesis by A2,A5,A9,A11,RLVECT_1:def 12;
end;
theorem Th16:
for R being Ring, S being Subring of R
for f being Polynomial of S
for r being Element of R, s being Element of S st r = s
holds Ext_eval(f,r) = Ext_eval(f,s)
proof
let R be Ring;
let S be Subring of R;
let f be Polynomial of S;
let r be Element of R;
let s be Element of S;
assume
A1: r = s;
consider F being FinSequence of R such that
A2: Ext_eval(f,r) = Sum F and
A3: len F = len f and
A4: for n being Element of NAT st n in dom F holds
F.n = In(f.(n-'1),R) * (power R).(r,n-'1) by ALGNUM_1:def 1;
consider G being FinSequence of S such that
A5: Ext_eval(f,s) = Sum G and
A6: len G = len f and
A7: for n being Element of NAT st n in dom G holds
G.n = In(f.(n-'1),S) * (power S).(s,n-'1) by ALGNUM_1:def 1;
now
let n such that
A8: n in dom F;
A9: dom F = dom G by A3,A6,FINSEQ_3:29;
A10: r = In(s,R) by A1;
A11: f.(n-'1)*(power S).(s,n-'1) is Element of R by Th7;
thus F.n = In(f.(n-'1),R)*(power R).(r,n-'1) by A4,A8
.= In(f.(n-'1)*(power S).(s,n-'1),R) by A10,ALGNUM_1:11
.= In(f.(n-'1),S) * (power S).(s,n-'1) by A11
.= G.n by A7,A8,A9;
end;
then F = G by A3,A6,FINSEQ_2:9; then
A12: In(Sum G,R) = Sum F by ALGNUM_1:10;
Sum G is Element of R by Th7;
hence Ext_eval(f,r) = Ext_eval(f,s) by A2,A5,A12;
end;
theorem
for R being Ring, S being Subring of R
for r being Element of R, s being Element of S
st r = s & s is_integral_over S holds r is_integral_over R
proof
let R be Ring;
let S be Subring of R;
let r be Element of R;
let s be Element of S;
assume
A1: r = s;
given f being Polynomial of S such that
A2: LC f = 1.S and
A3: Ext_eval(f,s) = 0.S;
reconsider f1 = f as Polynomial of R by Th8;
take f1;
LC f = LC f1 by Th9;
hence LC f1 = 1.R by A2,C0SP1:def 3;
r = In(r,R);
then Ext_eval(f1,r) = Ext_eval(f,r) by Th15
.= Ext_eval(f,s) by A1,Th16;
hence Ext_eval(f1,r) = 0.R by A3,C0SP1:def 3;
end;
theorem Th18:
for R being Ring, S being Subring of R
for r being Element of R, s being Element of S
for f being Polynomial of R, g being Polynomial of S
st r = s & f = g & r is_a_root_of f holds s is_a_root_of g
proof
let R be Ring;
let S be Subring of R;
let r be Element of R, s be Element of S;
let f be Polynomial of R, g be Polynomial of S;
assume that
A1: r = s and
A2: f = g and
A3: eval(f,r) = 0.R;
consider F being FinSequence of R such that
A4: eval(f,r) = Sum F and
A5: len F = len f and
A6: for n being Element of NAT st n in dom F
holds F.n = f.(n-'1) * (power R).(r,n-'1) by POLYNOM4:def 2;
A7: for n being Element of NAT st n in dom F
holds F.n = g.(n-'1) * (power S).(s,n-'1)
proof
let n be Element of NAT such that
A8: n in dom F;
A9: g.(n-'1)*(power S).(s,n-'1) is Element of R by Th7;
thus F.n = f.(n-'1)*(power R).(r,n-'1) by A6,A8
.= In(g.(n-'1),R)*(power R).(In(s,R),n-'1) by A1,A2
.= In(g.(n-'1)*(power S).(s,n-'1),R) by ALGNUM_1:11
.= g.(n-'1)*(power S).(s,n-'1) by A9;
end;
rng F c= the carrier of S
proof
let y be object;
assume y in rng F;
then consider n being object such that
A10: n in dom F and
A11: F.n = y by FUNCT_1:def 3;
reconsider n as Element of NAT by A10;
F.n = g.(n-'1) * (power S).(s,n-'1) by A7,A10;
hence thesis by A11;
end;
then reconsider G = F as FinSequence of S by FINSEQ_1:def 4;
A12: len G = len g by A2,A5,Th9;
Sum G is Element of R by Th7;
then Sum G = In(Sum G,R)
.= Sum F by ALGNUM_1:10
.= 0.S by A3,A4,C0SP1:def 3;
hence eval(g,s) = 0.S by A7,A12,POLYNOM4:def 2;
end;
theorem Th19:
for R being Ring holds R is Subring of R
proof
let R be Ring;
thus the carrier of R c= the carrier of R;
thus thesis;
end;
Lm1: 0.FC = 0 by COMPLFLD:def 1;
Lm2: 1.FC = 1 by COMPLFLD:def 1;
Lm3: FC is Subring of FC by Th19;
registration
cluster 0_.F_Complex -> INT -valued;
coherence by Lm1;
cluster 1_.F_Complex -> INT -valued;
coherence
proof
A1: rng 1_.FC c= rng 0_.FC \/ {1.FC} by FUNCT_7:100;
1.FC = 1 by COMPLFLD:def 1;
hence rng 1_.FC c= INT by A1,INT_1:def 2;
end;
end;
registration
let L be non degenerated non empty doubleLoopStr;
cluster monic -> non-zero for Polynomial of L;
coherence;
end;
registration
cluster monic INT -valued for Polynomial of F_Complex;
existence
proof
take 1_.FC;
thus thesis;
end;
cluster monic RAT-valued for Polynomial of F_Complex;
existence
proof
take 1_.FC;
thus thesis;
end;
cluster monic REAL-valued for Polynomial of F_Complex;
existence
proof
take 1_.FC;
thus thesis;
end;
end;
theorem Th20:
for f being INT -valued Polynomial of F_Complex holds
f is Polynomial of INT.Ring
proof
let f be INT -valued Polynomial of FC;
rng f c= INT by RELAT_1:def 19;
then reconsider f1 = f as sequence of IR by FUNCT_2:6;
f1 is finite-Support by Lm1,ALGSEQ_1:def 1;
hence thesis;
end;
theorem Th21:
for f being RAT-valued Polynomial of F_Complex holds
f is Polynomial of F_Rat
proof
let f be RAT-valued Polynomial of FC;
rng f c= RAT by RELAT_1:def 19;
then reconsider f1 = f as sequence of Fq by FUNCT_2:6;
f1 is finite-Support by Lm1,ALGSEQ_1:def 1;
hence thesis;
end;
theorem Th22:
for f being REAL-valued Polynomial of F_Complex holds
f is Polynomial of F_Real
proof
let f be REAL-valued Polynomial of FC;
rng f c= REAL;
then reconsider f1 = f as sequence of FR by FUNCT_2:6;
f1 is finite-Support by Lm1,ALGSEQ_1:def 1;
hence thesis;
end;
registration
let L be non empty ZeroStr;
cluster non-zero -> non zero for Polynomial of L;
correctness;
cluster zero -> non non-zero for Polynomial of L;
correctness;
end;
theorem Th23:
for i being Integer
for f being INT -valued FinSequence st i in rng f holds i divides Product f
proof
defpred P[FinSequence of INT] means for a being Integer st a in rng
$1 holds a divides Product $1;
A1: for p being FinSequence of INT, n being Element of INT st P[p] holds
P[p^<*n*>]
proof
let p be FinSequence of INT, n be Element of INT such that
A2: P[p];
set p1 = p^<*n*>;
A3: rng p1 = rng p \/ rng <*n*> by FINSEQ_1:31;
A4: Product p1 = Product p * n by RVSUM_1:96;
let a be Integer such that
A5: a in rng p1;
per cases by A5,A3,XBOOLE_0:def 3;
suppose a in rng p;
hence thesis by A2,A4,INT_2:2;
end;
suppose a in rng <*n*>;
then a in {n} by FINSEQ_1:39;
then a = n by TARSKI:def 1;
hence thesis by A4;
end;
end;
A6: P[<*>INT qua FinSequence of INT];
A7: for p being FinSequence of INT holds P[p] from FINSEQ_2:sch 2(A6,A1);
let i be Integer;
let f be INT -valued FinSequence;
rng f c= INT by RELAT_1:def 19;
then reconsider g=f as FinSequence of INT by FINSEQ_1:def 4;
P[g] by A7;
hence thesis;
end;
theorem Th24:
(ex f being non-zero INT -valued Polynomial of F_Complex st c is_a_root_of f)
iff
(ex f being monic RAT-valued Polynomial of F_Complex st c is_a_root_of f)
proof
thus (ex f being non-zero INT -valued Polynomial of FC st
c is_a_root_of f)
implies
(ex f being monic RAT-valued Polynomial of FC st c is_a_root_of f)
proof
given f being non-zero INT -valued Polynomial of FC such that
A1: c is_a_root_of f;
f <> 0_.FC; then
A2: len f <> 0 by POLYNOM4:5;
rng NormPolynomial(f) c= RAT
proof
let o be object;
assume o in rng NormPolynomial(f);
then consider x being object such that
A3: x in dom NormPolynomial(f) & o=(NormPolynomial(f)).x by FUNCT_1:def 3;
reconsider x as Element of NAT by A3;
reconsider fix=f.x, fil=f.(len f-'1) as Integer;
A4: f.(len f-'1) = LC(f);
o=f.x / f.(len f-'1) by A3,POLYNOM5:def 11
.= fix / fil by A4,COMPLFLD:6;
hence o in RAT by RAT_1:def 1;
end;
then
reconsider g=NormPolynomial(f) as monic RAT-valued Polynomial of FC
by RELAT_1:def 19;
take g;
thus c is_a_root_of g by A1,A2,POLYNOM5:59;
end;
given f being monic RAT-valued Polynomial of FC such that
A5: c is_a_root_of f;
f <> 0_.FC; then
A6: len f <> 0 by POLYNOM4:5;
reconsider lf=len f as Element of NAT;
deffunc F(Element of NAT) = In(denominator(f.$1),FC);
consider d being Polynomial of FC such that
A7: len d <= lf & for n being Element of NAT st n < lf holds d.n=F(n)
from POLYNOM3:sch 2;
now
assume A8: len d < lf;
then reconsider lf1=lf-1 as Element of NAT by NAT_1:20;
len d < lf1+1 by A8;
then
A9: len d <= lf1 by NAT_1:13;
d.lf1=F(lf1) by A7,XREAL_1:44;
then d.lf1 <> 0.FC by COMPLFLD:def 1;
hence contradiction by A9,ALGSEQ_1:8;
end;
then
A10: len d = len f by A7,XXREAL_0:1;
deffunc G(Nat) = d.($1-'1);
consider df being FinSequence such that
A11: len df = len d & for k being Nat st k in dom df holds df.k=G(k)
from FINSEQ_1:sch 2;
A12: rng df c= INT
proof
let o be object;
assume o in rng df;
then consider a being object such that
A13: a in dom df & o=df.a by FUNCT_1:def 3;
reconsider a as Element of NAT by A13;
A14: 1 <= a & a <= len df by A13,FINSEQ_3:25;
then a-'1 = a-1 by XREAL_0:def 2;
then
A15: a-'1 < len f by A10,A11,A14,XREAL_1:231;
df.a=d.(a-'1) by A13,A11
.= In(denominator(f.(a-'1)),FC) by A15,A7
.= denominator(f.(a-'1));
hence o in INT by A13,INT_1:def 2;
end;
then reconsider df as INT -valued FinSequence by RELAT_1:def 19;
rng df c= COMPLEX by A12,NUMBERS:16;
then rng df c= the carrier of FC by COMPLFLD:def 1; then
reconsider dfc=df as FinSequence of FC by FINSEQ_1:def 4;
Product df in COMPLEX by XCMPLX_0:def 2;
then reconsider dd=Product df as Element of FC by COMPLFLD:def 1;
A16: for i being Nat st i in dom dfc holds dfc.i <> 0.FC
proof
let i be Nat;
assume A17: i in dom dfc;
then reconsider a=i as Element of NAT;
A18: 1 <= a & a <= len df by A17,FINSEQ_3:25;
then a-'1 = a-1 by XREAL_0:def 2;
then
A19: a-'1 < len f by A10,A11,A18,XREAL_1:231;
df.a=d.(a-'1) by A17,A11
.= In(denominator(f.(a-'1)),FC) by A19,A7
.= denominator(f.(a-'1));
hence dfc.i <> 0.FC by COMPLFLD:def 1;
end;
A20: the multF of FC = multcomplex & the carrier of FC = COMPLEX
by COMPLFLD:def 1;
consider dfo being FinSequence of COMPLEX such that
A21: dfo=df & Product df = multcomplex $$ dfo by RVSUM_1:def 13;
Product df = Product dfc by A20,A21,GROUP_4:def 2;
then
A22: len (dd*f) > 0 by A16,A6,POLYNOM5:25,RING_2:2;
rng (dd*f) c= INT
proof
let o be object;
assume o in rng (dd*f);
then consider a being object such that
A23: a in dom (dd*f) & o=(dd*f).a by FUNCT_1:def 3;
reconsider a as Element of NAT by A23;
A24: o=dd*f.a by A23,POLYNOM5:def 4
.= (Product df) * (f.a);
per cases;
suppose a >= len f;
then f.a = 0.FC by ALGSEQ_1:8;
then o =(Product df)*0 by A24,COMPLFLD:def 1
.= 0;
hence o in INT by INT_1:def 2;
end;
suppose
A25: a < len f;
then
A26: 1 <= a+1 & a+1 <= len df by A11,A10,NAT_1:12,13;
then
A27: a+1 in dom df by FINSEQ_3:25;
df.(a+1) = d.(a+1-'1) by A11,A26,FINSEQ_3:25
.= d.a by NAT_D:34
.= In(denominator(f.a),FC) by A25,A7
.= denominator(f.a);
then denominator(f.a) in rng df by A27,FUNCT_1:def 3;
then denominator(f.a) divides Product df by Th23;
then consider j being Integer such that
A28: Product df = denominator(f.a) * j;
f.a = numerator(f.a)/denominator(f.a);
then o = j*numerator(f.a) by A28,A24,XCMPLX_1:90;
hence o in INT by INT_1:def 2;
end;
end;
then reconsider g=dd*f as non-zero INT -valued Polynomial of FC
by RELAT_1:def 19,UPROOTS:17,A22;
take g;
eval(g,c)=dd*0.FC by A5,POLYNOM5:30;
hence c is_a_root_of g;
end;
theorem Th25:
c is algebraic iff
ex f being monic RAT-valued Polynomial of F_Complex st c is_a_root_of f
proof
hereby
assume c is algebraic;
then c is_integral_over Fq;
then consider f being Polynomial of Fq such that
A1: LC f = 1.Fq and
A2: Ext_eval(f,c) = 0.FC;
reconsider f1 = f as RAT-valued Polynomial of FC by ALGNUM_1:3,Th8;
f1 is monic by A1,Th9,Lm2,ALGNUM_1:3;
then reconsider f1 as monic RAT-valued Polynomial of FC;
take f1;
thus c is_a_root_of f1
proof
thus eval(f1,c) = In(eval(f1,c),FC)
.= Ext_eval(f1,In(c,FC)) by Lm3,ALGNUM_1:12
.= 0.FC by A2,Th15,ALGNUM_1:3;
end;
end;
given f1 being monic RAT-valued Polynomial of FC such that
A3: c is_a_root_of f1;
reconsider f = f1 as Polynomial of Fq by Th21;
take f;
LC f1 = 1.FC by RATFUNC1:def 7;
hence LC f = 1.Fq by Th9,Lm2,ALGNUM_1:3;
thus Ext_eval(f,c) = Ext_eval(f1,In(c,FC)) by Th15,ALGNUM_1:3
.= In(eval(f1,c),FC) by Lm3,ALGNUM_1:12
.= 0.FC by A3;
end;
theorem Th26:
c is algebraic iff
ex f being non-zero INT -valued Polynomial of F_Complex st c is_a_root_of f
proof
hereby
assume c is algebraic;
then ex f being monic RAT-valued Polynomial of FC
st c is_a_root_of f by Th25;
hence
ex f being non-zero INT -valued Polynomial of FC st c is_a_root_of f
by Th24;
end;
assume
ex f being non-zero INT -valued Polynomial of FC st c is_a_root_of f;
then ex f being monic RAT-valued Polynomial of FC
st c is_a_root_of f by Th24;
hence thesis by Th25;
end;
theorem Th27:
c is algebraic_integer iff
ex f being monic INT -valued Polynomial of F_Complex st c is_a_root_of f
proof
hereby
assume c is algebraic_integer;
then c is_integral_over IR;
then consider f being Polynomial of IR such that
A1: LC f = 1.IR and
A2: Ext_eval(f,c) = 0.FC;
reconsider f1 = f as RAT-valued Polynomial of FC by ALGNUM_1:4,Th8;
f1 is monic by A1,Th9,Lm2,ALGNUM_1:4;
then reconsider f1 as monic INT -valued Polynomial of FC;
take f1;
thus c is_a_root_of f1
proof
thus eval(f1,c) = In(eval(f1,c),FC)
.= Ext_eval(f1,In(c,FC)) by Lm3,ALGNUM_1:12
.= 0.FC by A2,Th15,ALGNUM_1:4;
end;
end;
given f1 being monic INT -valued Polynomial of FC such that
A3: c is_a_root_of f1;
reconsider f = f1 as Polynomial of IR by Th20;
take f;
LC f1 = 1.FC by RATFUNC1:def 7;
hence LC f = 1.IR by Th9,Lm2,ALGNUM_1:4;
thus Ext_eval(f,c) = Ext_eval(f1,In(c,FC)) by Th15,ALGNUM_1:4
.= In(eval(f1,c),FC) by Lm3,ALGNUM_1:12
.= 0.FC by A3;
end;
registration
cluster algebraic_integer -> algebraic for Complex;
coherence
proof
let c be Complex;
assume
A1: c is algebraic_integer;
c in COMPLEX by XCMPLX_0:def 2;
then reconsider c as Element of FC by COMPLFLD:def 1;
ex f being monic INT -valued Polynomial of FC st c is_a_root_of f
by A1,Th27;
hence thesis by Th26;
end;
cluster transcendental -> non algebraic_integer for Complex;
coherence;
end;
::$N Liouville's theorem on diophantine approximation
::$L https://en.wikipedia.org/wiki/Liouville_number Liouville number
theorem Th28:
for f being non-zero INT -valued Polynomial of F_Real
for a being irrational Element of F_Real st a is_a_root_of f
ex A being positive Real st
for p being Integer, q being positive Nat holds
|. a-p/q .| > A/(q|^len f)
proof
let f be non-zero INT -valued Polynomial of FR;
set n = len f;
let a be irrational Element of FR;
assume
A1: a is_a_root_of f;
set X = [. a-1,a+1 .];
set E = Eval(f);
set F = E`| |X;
set M1 = sup rng |.F.|;
A2: dom E = REAL by FUNCT_2:def 1;
A3: E is differentiable;
A4: dom(E`|) = REAL by FUNCT_2:def 1;
then
A5: dom F = X by RELAT_1:62;
A6: dom |.F.| = dom F by VALUED_1:def 11;
reconsider F as PartFunc of X,REAL by RELAT_1:185;
F is bounded by A4,INTEGRA5:10;
then rng |.F.| is real-bounded by INTEGRA1:15;
then reconsider M1 as Element of REAL by XXREAL_2:16;
set M = M1+1;
consider Y being object such that
A7: Y in rng |.F.| by XBOOLE_0:def 1;
reconsider Y as Real by A7;
consider A being object such that
A in dom |.F.| and
A8: |.F.|.A = Y by A7,FUNCT_1:def 3;
A9: |.F.|.A = |.F.A.| by VALUED_1:18;
M1 is UpperBound of rng |.F.| by XXREAL_2:def 3;
then
A10: Y <= M1 by A7,XXREAL_2:def 1;
A11: M1+0 <= M by XREAL_1:6;
set RTS = Roots(f) \ {a};
deffunc F(Real) = |.a-$1.|;
set DIF = {F(b) where b is Element of FR : b in RTS};
A12: RTS is finite;
A13: DIF is finite from FRAENKEL:sch 21(A12);
DIF c= REAL
proof
let x be object;
assume x in DIF;
then ex b being Element of FR st x = F(b) & b in RTS;
hence thesis by XREAL_0:def 1;
end;
then reconsider DIF as finite Subset of REAL by A13;
set MIN = {1,1/M} \/ DIF;
MIN c= REAL by XREAL_0:def 1;
then reconsider MIN as finite non empty Subset of REAL;
for x being Real st x in MIN holds x > 0
proof
let x be Real;
assume x in MIN;
then x in {1,1/M} or x in DIF by XBOOLE_0:def 3;
then per cases by TARSKI:def 2;
suppose x = 1 or x = 1/M;
hence thesis by A10,A9,A8;
end;
suppose ex b being Element of FR st x = F(b) & b in RTS;
then consider b being Element of FR such that
A14: x = F(b) and
A15: b in RTS;
a-b <> 0 by A15,ZFMISC_1:56;
hence thesis by A14;
end;
end;
then min MIN > 0 by XXREAL_2:def 5;
then consider A being Real such that
A16: 0 < A and
A17: A < inf MIN by XREAL_1:5;
reconsider A as positive Real by A16;
take A;
let p be Integer;
let q be positive Nat;
set qn = q|^n;
reconsider qtn=qn as Element of FR by XREAL_0:def 1;
assume
A18: |. a-p/q.| <= A/qn;
A19: |. a-p/q.| = |. p/q-a.| by COMPLEX1:60;
A20: E.a = 0.FR by A1,POLYNOM5:def 13;
reconsider pq = p/q as Element of FR by XREAL_0:def 1;
0+1 <= qn by NAT_1:13;
then A/qn <= A/1 by XREAL_1:118;
then |.a-p/q.| <= A by A18,XXREAL_0:2;
then
A21: |.a-p/q.| < inf MIN by A17,XXREAL_0:2;
then not |.a-p/q.| in MIN by XXREAL_2:3;
then not |.a-p/q.| in DIF by XBOOLE_0:def 3;
then not pq in RTS;
then not p/q in Roots(f) by ZFMISC_1:56;
then
A22: not pq is_a_root_of f by POLYNOM5:def 10;
A23: E.(p/q) = eval(f,pq) & E.(a) = eval(f,a) by POLYNOM5:def 13;
A24: a+0 <= a+1 by XREAL_1:6;
A25: 1 / (M*qn) = (1/M) * (1/qn) by XCMPLX_1:102;
1/M in {1,1/M} by TARSKI:def 2;
then 1/M in MIN by XBOOLE_0:def 3;
then inf MIN <= 1/M by XXREAL_2:3;
then A < 1/M by A17,XXREAL_0:2;
then
A26: A*(1/qn) < (1/M)*(1/qn) by XREAL_1:68;
1 in {1,1/M} by TARSKI:def 2;
then 1 in MIN by XBOOLE_0:def 3;
then inf MIN <= 1 by XXREAL_2:3;
then
A27: |.a-p/q.| <= 1 by A21,XXREAL_0:2;
consider EF being FinSequence of the carrier of FR such that
A28: E.(p/q) = Sum EF & len EF = len f & for n be Element of NAT st n in
dom EF holds EF.n = f.(n-'1) * (power FR).(pq,n-'1) by POLYNOM4:def 2,A23;
set G = qtn*EF;
reconsider FF=EF as Element of (len EF)-tuples_on the carrier of F_Real
by FINSEQ_2:92;
set GG=qtn*FF;
len GG = len EF by FINSEQ_2:132;
then
A29: dom G = Seg (len EF) by FINSEQ_1:def 3 .= dom EF by FINSEQ_1:def 3;
rng G c= INT
proof
let o be object;
assume o in rng G;
then consider b being object such that
A30: b in dom G & o=G.b by FUNCT_1:def 3;
reconsider b as Element of NAT by A30;
b in Seg n by A30,A29,A28,FINSEQ_1:def 3;
then 1 <= b & b <= n & b-'1 <= b by FINSEQ_1:1,NAT_D:35;
then consider c being Nat such that
A31: n = b-'1+c by NAT_1:10,XXREAL_0:2;
rng EF c= the carrier of F_Real; then
reconsider a9=EF.b as Element of F_Real by A30,A29,FUNCT_1:3;
b in dom (qtn*EF) & a9 = EF.b implies (qtn*EF).b = qtn*a9
by FVSUM_1:50;
then
G.b = qtn*(f.(b-'1) * (power F_Real).(pq,b-'1)) by A28,A30,A29
.= f.(b-'1) * ((q|^n) * (power F_Real).(pq,b-'1))
.= f.(b-'1) * ((q|^n) * ((p/q)|^(b-'1))) by NIVEN:7
.= f.(b-'1) * ((q|^n) * ((p|^(b-'1))/(q|^(b-'1)))) by PREPOWER:8
.= f.(b-'1) * (p|^(b-'1)) * ((q|^n)/(q|^(b-'1)))
.= f.(b-'1) * (p|^(b-'1)) * ((q|^c)*(q|^(b-'1))/(q|^(b-'1)))
by A31,NEWTON:8
.= f.(b-'1) * (p|^(b-'1)) * ((q|^c)*((q|^(b-'1))/(q|^(b-'1))))
.= f.(b-'1) * (p|^(b-'1)) * ((q|^c) * 1) by XCMPLX_1:60
.= f.(b-'1) * (p|^(b-'1)) * (q|^c);
hence o in INT by INT_1:def 2,A30;
end;
then reconsider G1=G as INT -valued FinSequence by RELAT_1:def 19;
Sum G1 = Sum G by NIVEN:6;
then reconsider SG=Sum G as Integer;
Sum G = qtn*Sum EF by FVSUM_1:73
.= qn*Sum EF;
then |.SG.| = |.qn.| * |.Sum EF.| by COMPLEX1:65;
then
A32: |.E.(p/q).| >= 1/qn by A28,A22,A23,NAT_1:14,XREAL_1:79;
per cases by XXREAL_0:1;
suppose
A33: p/q < a;
E | [. p/q,a .] is continuous;
then consider x0 being Real such that
A34: x0 in ]. p/q,a .[ and
A35: diff(E,x0) = (E.a-E.(p/q)) / (a-p/q) by A2,A3,A33,FDIFF_1:26,ROLLE:3;
A36: |.E.a-E.(p/q).| = |.E.(p/q).| by A20,COMPLEX1:52;
A37: a-p/q <> 0;
then a-p/q = (E.a-E.(p/q)) / diff(E,x0) by A35,A1,A22,A23,XCMPLX_1:54;
then
A38: |.a-p/q.| = |.E.(p/q).| / |.diff(E,x0).| by A36,COMPLEX1:67;
a-p/q <= 1 by A27,ABSVALUE:5;
then a-p/q-a <= 1-a by XREAL_1:9;
then -(-p/q) >= -(1-a) by XREAL_1:24;
then
A39: ]. p/q,a .[ c= X by A24,XXREAL_1:37;
then
A40: F.x0 = (E`|).x0 by A34,FUNCT_1:49
.= diff(E,x0) by POLYDIFF:10;
|.F.|.x0 = |.F.x0 .| by VALUED_1:18;
then |.diff(E,x0).| in rng |.F.| by A5,A6,A34,A39,A40,FUNCT_1:def 3;
then |.diff(E,x0).| <= M1 by XXREAL_2:4;
then |.diff(E,x0).| <= M by A11,XXREAL_0:2;
then 1 / |.diff(E,x0).| >= 1/M by A35,A1,A37,A22,A23,XREAL_1:118;
then |.E.(p/q).| / |.diff(E,x0).| >= 1/(M*qn)
by A10,A9,A8,A32,A25,XREAL_1:66;
hence contradiction by A18,A38,A25,A26,XXREAL_0:2;
end;
suppose
A41: a < p/q;
E | [. a,p/q .] is continuous;
then consider x0 being Real such that
A42: x0 in ]. a,p/q .[ and
A43: diff(E,x0) = (E.(p/q)-E.a) / (p/q-a) by A2,A3,A41,FDIFF_1:26,ROLLE:3;
A44: p/q-a <> 0;
then p/q-a = (E.(p/q)-E.a) / diff(E,x0) by A1,A22,A23,A43,XCMPLX_1:54;
then
A45: |.p/q-a.| = |.E.(p/q).| / |.diff(E,x0).| by A20,COMPLEX1:67;
A46: a-1 < a-0 by XREAL_1:15;
-1 <= a-p/q by A27,ABSVALUE:5;
then -1-a <= a-p/q-a by XREAL_1:9;
then -(-1-a) >= -(-p/q) by XREAL_1:24;
then
A47: ]. a,p/q .[ c= X by A46,XXREAL_1:37;
then
A48: F.x0 = (E`|).x0 by A42,FUNCT_1:49
.= diff(E,x0) by POLYDIFF:10;
|.F.|.x0 = |.F.x0 .| by VALUED_1:18;
then |.diff(E,x0).| in rng |.F.| by A5,A6,A42,A47,A48,FUNCT_1:def 3;
then |.diff(E,x0).| <= M1 by XXREAL_2:4;
then |.diff(E,x0).| <= M by A11,XXREAL_0:2;
then 1 / |.diff(E,x0).| >= 1/M by A43,A1,A22,A44,A23,XREAL_1:118;
then |.E.(p/q).| / |.diff(E,x0).| >= 1/(M*qn)
by A10,A9,A8,A25,A32,XREAL_1:66;
hence contradiction by A18,A19,A45,A25,A26,XXREAL_0:2;
end;
end;
Lm4:
now
let n;
let L be Liouville;
let A be positive Real such that
A1: for p being Integer, q being positive Nat holds
|. L-p/q .| > A/(q|^n);
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;
end;
::$N All Liouville numbers are transcendental
::$L https://en.wikipedia.org/wiki/Liouville_number Liouville number
registration
cluster -> transcendental for Liouville;
coherence
proof
let L be Liouville;
assume L is algebraic;
then consider f being non-zero INT -valued Polynomial of FC such that
A1: In(L,FC) is_a_root_of f by Th26;
reconsider g = f as non-zero INT -valued Polynomial of FR by Th4,Th13,Th22;
L is irrational Element of FR by XREAL_0:def 1;
then ex A being positive Real st
for p being Integer, q being positive Nat holds
|. L-p/q .| > A/(q|^len g) by A1,Th4,Th18,Th28;
hence thesis by Lm4;
end;
end;