:: 1. Define Liouville numbers :: 2. Show that in the definition of Liouville numbers taken from Wikipedia :: the quantification of n can be replaced from "every positive integer" :: into "non-zero natural number". :: 3. Prove auxiliary lemma that powers of two are unbounded, i.e., :: for any integer d, there exists a non-zero natural number :: such that 2 to_power (n - 1) > d. :: 4. Prove that no Liouville number can be rational (follow the proof :: from Wikipedia). environ vocabularies CICM9, NUMBERS, SUBSET_1, INT_1, SEQ_1, FINSEQ_1, RAT_1, ORDINAL4, POWER, INT_2, SQUARE_1, XXREAL_0, CARD_1, ARYTM_3, RELAT_1, NAT_1, FUNCT_1, ARYTM_1, REALSET1, SEQ_2, ORDINAL2, COMPLEX1, VALUED_1, SERIES_1, CARD_3, XBOOLE_0, RFINSEQ, PARTFUN1, FINSEQ_2, NEWTON, SIN_COS, IRRAT_1, REAL_1, ASYMPT_1, XCMPLX_0, FUNCT_7, TARSKI, PREPOWER, ABIAN, ORDINAL1, FUNCT_4, FUNCOP_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, RELAT_1, REAL_1, INT_1, COMPLEX1, SQUARE_1, FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_4, ABSVALUE, VALUED_0, VALUED_1, FUNCT_2, NAT_1, SEQ_1, COMSEQ_2, SEQ_2, PREPOWER, POWER, FINSEQ_1, RVSUM_1, SERIES_1, FINSEQ_2, RFINSEQ, SIN_COS, RAT_1, INT_2, PEPIN, NEWTON, IRRAT_1, ABIAN, ASYMPT_1; constructors ARYTM_0, REAL_1, NAT_1, NAT_D, SEQ_2, PARTFUN1, RVSUM_1, ABSVALUE, IRRAT_1, FUNCT_1, ASYMPT_1, PREPOWER, ABIAN, FUNCT_4, LIMFUNC1, COMSEQ_3, RFINSEQ, BINARITH, SIN_COS, PEPIN, SERIES_1, POWER, RELSET_1, COMSEQ_2, SEQ_1, NUMBERS, FUNCOP_1, FUNCT_2; registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, POWER, FINSEQ_1, SQUARE_1, RVSUM_1, SEQ_1, SEQ_2, CARD_1, ABSVALUE, XCMPLX_0, FUNCT_1, PREPOWER, NUMPOLY1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; equalities SEQ_1; definitions TARSKI, XBOOLE_0, FINSEQ_1; theorems RAT_1, INT_1, POWER, ENTROPY1, NAT_1, XXREAL_0, XCMPLX_1, ABSVALUE, COMPLEX1, XREAL_1, HOLDER_1, FUNCT_2, NEWTON, RELAT_1, FUNCT_1, FUNCOP_1, FUNCT_4, XBOOLE_1, SERIES_1, SIN_COS, RVSUM_1, RFINSEQ, FINSEQ_2, IRRAT_1, SEQ_4, ORDINAL1, SEQ_1, FINSEQ_1, VALUED_1, XBOOLE_0, XREAL_0, FINSEQ_3; schemes NAT_1, SEQ_1, IRRAT_1; begin :: HOLDER_1:3 revised theorem HOLDER13: for p be Real st 0 <= p :: originally: 0 < p for a,b be Real st 0 <= a & a <= b holds a to_power p <= b to_power p :: by HOLDER_1:3 proof let p be Real such that A1: 0 <= p; let a, b be Real such that A2: 0 <= a and A3: a <= b; per cases by A1; suppose S1: 0 = p; a to_power 0 = 1 & b to_power 0 = 1 by POWER:24; hence thesis by S1; end; suppose S2: 0 < p; per cases; suppose a = b; hence thesis; end; suppose A4: a <> b; A5: a < b by A3,A4,XXREAL_0:1; now per cases; suppose A6: a = 0; then a to_power p = 0 by S2,POWER:def 2; hence thesis by A3,A4,A6,POWER:34; end; suppose a <> 0; hence thesis by A2,A5,S2,POWER:37; end; end; hence thesis; end; end; end; begin :: Potentially useful MML theorems theorem :: XREAL_1:72 for a,b,c being Real holds 0 <= c & b <= a implies b/c <= a/c by XREAL_1:72; theorem :: XREAL_1:76 for a,b,c being Real holds 0 < c & 0 < a & a < b implies c/b < c/a by XREAL_1:76; theorem :: XREAL_1:118 for a,b,c being Real holds 0 < a & 0 <= c & a <= b implies c/b <= c/a by XREAL_1:118; theorem :: XXREAL_0:2 for a,b,c being Real holds a <= b & b <= c implies a <= c by XXREAL_0:2; theorem :: XXREAL_0:1 for a,b being Real holds a <= b & b <= a implies a = b by XXREAL_0:1; theorem :: XREAL_1:11 for a,b,c being Real holds a <= b-c implies c <= b-a by XREAL_1:11; theorem :: XCMPLX_1:130 for a,b,c,d being Real holds b <> 0 & d <> 0 implies a / b - c / d = (a * d - c * b) / (b * d) by XCMPLX_1:130; theorem :: XCMPLX_1:94 for a,b,c,d being Real holds c <> 0 & d <> 0 & a * c = b * d implies a / d = b / c by XCMPLX_1:94; theorem :: ABSVALUE:2 for x being Real holds x = 0 iff |.x.| = 0 by ABSVALUE:2; theorem :: COMPLEX1:67 for z1,z2 being Real holds |.z1.| / |.z2.| = |.z1/z2.| by COMPLEX1:67; :: Integer numbers theorem :: INT_1:3 for i0 being Integer holds 0 <= i0 implies i0 in NAT by INT_1:3; theorem :: NAT_1:13 for i,j being Nat holds i < j + 1 iff i <= j by NAT_1:13; theorem :: INT_1:7 for i0, i1 being Integer holds i0 < i1 implies i0 + 1 <= i1 by INT_1:7; theorem :: NAT_1:14 for i being Nat holds i < 1 implies i = 0 by NAT_1:14; :: Power and logarithm function theorem :: NEWTON:4 for z being Real holds z |^ 0 = 1 by NEWTON:4; theorem :: POWER:24 for a being Real holds a to_power 0 = 1 by POWER:24; theorem :: POWER:34 for a, b being Real holds a > 0 implies a to_power b > 0 by POWER:34; theorem :: ENTROPY1:4 for a,b being Real holds a>1 & b>1 implies log(a,b) > 0 by ENTROPY1:4; theorem :: POWER:27 for a,b,c being Real holds a > 0 implies a to_power (b+c) = a to_power b * a to_power c by POWER:27; theorem for a,b being Real st a>0 & a<>1 & b>0 holds a to_power log(a,b) = b by POWER:def 3; :: Ceiling function theorem for r being Real holds r <= [/ r \] & [/ r \] < r + 1 by INT_1:def 7; theorem :: INT_1:32 for r being Real holds r - 1 < [/ r \] & r < [/ r \] + 1 by INT_1:32; :: Rational numbers theorem for r being object holds r is rational iff r in RAT by RAT_1:def 2; theorem :: RAT_1:8 for p being Rational ex m being Integer, k being Nat st k<>0 & p=m/k by RAT_1:8; begin :: Liouville numbers definition let x be Real; attr x is liouville means for n being Nat ex p being Integer, q being Nat st q > 1 & 0 < |. x - p / q .| < 1 / (q |^ n); end; ::: Exercise 1: In the definition above the quantification of n ::: can be over non-zero natural numbers theorem LiouvilleEquivalent: for r being Real holds r is liouville iff for n being non zero Nat ex p being Integer, q being Nat st 1 < q & 0 < |. r - p/q .| < 1 / (q |^ n) proof let r be Real; thus r is liouville implies for n being non zero Nat ex p being Integer, q being Nat st 1 < q & 0 < |. r-p/q .| < 1 / (q |^ n); assume Z1: for n being non zero Nat ex p being Integer, q being Nat st 1 < q & 0 < |. r - p/q .| < 1 / (q |^ n); let n be Nat; per cases; suppose n is non zero; hence thesis; ::> *4 end; suppose A1: n is zero; consider p being Integer, q being Nat such that A2: 1 < q and A3: 0 < |. r-p/q .| and A4: |. r-p/q .| < 1/(q|^1); ::> *4 take p,q; thus 1 < q & 0 < |. r-p/q .|; ::> *4,4 hence thesis; ::> *4 end; end; :: Exercise 2: Lemma: Powers of 2 are unbounded theorem Lemma1: for d being Integer holds ex n being non zero Nat st 2 to_power (n - 1) > d proof let d be Integer; per cases; suppose C1: d <= 0; thus thesis; ::> *4 end; suppose C0: d > 0; set n = [/ log (2,d) \] + 2; reconsider n as non zero Nat; ::> *4,4 take n; thus thesis; ::> *4 end; end; ::: Exercise 3: Show that all Liouville numbers are irrational registration cluster liouville -> irrational for Real; coherence proof let x be Real; assume A0: x is liouville; assume x is rational; then x in RAT by RAT_1:def 2; then consider c being Integer, d being Nat such that A1: d <> 0 & x = c / d by RAT_1:8; consider n being non zero Nat such that ST: 2 to_power (n - 1) > d by Lemma1; :: Otherwise you can take appropriate constant thus thesis; ::> *1 end; end; definition let a be Nat; func Liouville_seq a -> Real_Sequence means it.0 = 0 & for n being non zero Nat holds it.n = a to_power (-n!); :: The same can be obtained with the more general definition existence; uniqueness; end; definition let a be Nat; func Liouville_constant a -> Real equals Sum Liouville_seq a; coherence; end; registration let a be non zero Nat; cluster Liouville_constant a -> liouville; coherence; ::> *4 end; registration cluster liouville for Real; existence proof take Liouville_constant 1; thus thesis; end; end; definition mode Liouville is liouville Real; end; 1 is not Liouville; ::> ::> 1: It is not true ::> 4: This inference is not accepted