:: All Liouville Numbers are Transcendental
:: by Artur Korni{\l}owicz , Adam Naumowicz and Adam Grabowski
::
:: Received February 23, 2017
:: Copyright (c) 2017 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, 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;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve m,n for Nat;
reserve r for Real;
reserve c for Element of F_Complex;
registration
let f be non empty complex-valued Function;
cluster |. f .| -> non empty;
end;
theorem :: LIOUVIL2:1
2 <= m implies for A being Real
ex n being positive Nat st A <= m|^n;
theorem :: LIOUVIL2:2
for A being positive Real
ex n being positive Nat st 1/(2|^n) <= A;
registration
let r,n;
cluster [.r-n,r+n.] -> right_end;
end;
registration
let a,b be Real;
cluster [.a,b.] -> closed_interval for Subset of REAL;
end;
registration
cluster irrational for Element of F_Real;
end;
theorem :: LIOUVIL2:3
F_Real is Subring of F_Complex;
theorem :: LIOUVIL2:4
F_Rat is Subring of F_Real;
theorem :: LIOUVIL2:5
INT.Ring is Subring of F_Real;
theorem :: LIOUVIL2:6
for R being Ring, S being Subring of R
for x being Element of S holds x is Element of R;
theorem :: LIOUVIL2:7
for R being Ring, S being Subring of R
for f being Polynomial of S holds
f is Polynomial of R;
theorem :: LIOUVIL2:8
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;
theorem :: LIOUVIL2:9
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;
theorem :: LIOUVIL2:10
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;
registration
let R be non degenerated Ring;
cluster -> non degenerated for Subring of R;
cluster non degenerated for Subring of R;
end;
theorem :: LIOUVIL2:11
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;
theorem :: LIOUVIL2:12
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;
theorem :: LIOUVIL2:13
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;
theorem :: LIOUVIL2:14
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));
theorem :: LIOUVIL2:15
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);
theorem :: LIOUVIL2:16
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;
theorem :: LIOUVIL2:17
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;
theorem :: LIOUVIL2:18
for R being Ring holds R is Subring of R;
registration
cluster 0_.F_Complex -> INT -valued;
cluster 1_.F_Complex -> INT -valued;
end;
registration
let L be non degenerated non empty doubleLoopStr;
cluster monic -> non-zero for Polynomial of L;
end;
registration
cluster monic INT -valued for Polynomial of F_Complex;
cluster monic RAT-valued for Polynomial of F_Complex;
cluster monic REAL-valued for Polynomial of F_Complex;
end;
theorem :: LIOUVIL2:19
for f being INT -valued Polynomial of F_Complex holds
f is Polynomial of INT.Ring;
theorem :: LIOUVIL2:20
for f being RAT-valued Polynomial of F_Complex holds
f is Polynomial of F_Rat;
theorem :: LIOUVIL2:21
for f being REAL-valued Polynomial of F_Complex holds
f is Polynomial of F_Real;
registration
let L be non empty ZeroStr;
cluster non-zero -> non zero for Polynomial of L;
cluster zero -> non non-zero for Polynomial of L;
end;
theorem :: LIOUVIL2:22
for i being Integer
for f being INT -valued FinSequence st i in rng f holds i divides Product f;
theorem :: LIOUVIL2:23
(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);
theorem :: LIOUVIL2:24
c is algebraic iff
ex f being monic RAT-valued Polynomial of F_Complex st c is_a_root_of f;
theorem :: LIOUVIL2:25
c is algebraic iff
ex f being non-zero INT -valued Polynomial of F_Complex st c is_a_root_of f;
theorem :: LIOUVIL2:26
c is algebraic_integer iff
ex f being monic INT -valued Polynomial of F_Complex st c is_a_root_of f;
registration
cluster algebraic_integer -> algebraic for Complex;
cluster transcendental -> non algebraic_integer for Complex;
end;
::$N Liouville's theorem on diophantine approximation
theorem :: LIOUVIL2:27
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);
::$N All Liouville numbers are transcendental
registration
cluster -> transcendental for Liouville;
end;