:: 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 by Z1; 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) by Z1; take p,q; thus 1 < q & 0 < |. r-p/q .| by A2,A3; A5: q |^ 0 = 1 by NEWTON:4; 1/q < 1/1 by A2,XREAL_1:76; hence thesis by A1,A4,A5,XXREAL_0:2; 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; take n = 1; 2 to_power (n - 1) = 2 to_power 0 .= 1 by POWER:24; hence thesis by C1; end; suppose C0: d > 0; then d >= 1 + 0 by INT_1:7; then d = 1 or d > 1 by XXREAL_0:1; then per cases; suppose C1: d = 1; take n = 2; 2 to_power (n - 1) = 2 to_power 1 .= 2; hence thesis by C1; end; suppose d > 1; then B1: log (2,d) > 0 by ENTROPY1:4; then [/ log (2,d) \] >= log (2,d) by INT_1:def 7; then B2: [/ log (2,d) \] > 0 by B1; set n = [/ log (2,d) \] + 2; AA: n > 0 by B2; then n in NAT by INT_1:3; then reconsider n as non zero Nat by AA; take n; A2: 2 > 0 & d > 0 by C0; n - 1 = [/ log (2,d) \] + 1; then n - 1 > log (2,d) by INT_1:32; then A3: 2 to_power (n - 1) > 2 to_power (log (2,d)) by POWER:39; 2 to_power (log (2,d)) = d by A2,POWER:def 3; hence thesis by A3; end; 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; consider p being Integer, q being Nat such that B1: q > 1 & 0 < |. x - p / q .| < 1 / (q |^ n) by A0; T1: q <> 0 by B1; T2: d <> 0 by A1; SS: |. c/d - p/q .| = |. (c * q - p * d) / (d * q) .| by XCMPLX_1:130,T1,T2 .= |. (c * q - p * d) .| / |. d * q .| by COMPLEX1:67 .= |. (c * q - p * d) .| / (d * q); c * q - p * d <> 0 proof assume c * q - p * d = 0; then p * d = c * q; then T3: p / q = c / d by XCMPLX_1:94,T1,T2; |. x - p/q .| = |. c/d - p/q .| by A1 .= 0 by T3; hence thesis by B1; end; then |. c * q - p * d .| <> 0 by ABSVALUE:2; then |. c * q - p * d .| >= 1 by NAT_1:14; then |. c * q - p * d .| / (d * q) >= 1 / (d * q) by XREAL_1:72; then HR: |. x - p / q .| >= 1 / (d * q) by SS,A1; d * q <> 0 by T1,T2; QW: d * q > 0 by T2,B1; q > 0 by B1; then d * q < (2 to_power (n - 1)) * q by ST,XREAL_1:68; then 1 / (d * q) > 1 / ((2 to_power (n - 1)) * q) by XREAL_1:76,QW; then HG: |. x - p / q .| >= 1 / ((2 to_power (n - 1)) * q) by HR,XXREAL_0:2; FG: 2 to_power (n - 1) > 0 by POWER:34; n - 0 >= 1 by NAT_1:14; then FO: n - 1 >= 0 by XREAL_1:11; 1 + 1 <= q by B1,NAT_1:13; then 2 to_power (n - 1) <= q to_power (n - 1) by FO,HOLDER13; then (2 to_power (n - 1)) * q <= (q to_power (n - 1)) * q by XREAL_1:66,FG; then (2 to_power (n - 1)) * q <= (q to_power (n - 1)) * (q to_power 1); then (2 to_power (n - 1)) * q <= (q to_power (n - 1 + 1)) by B1,POWER:27; then (2 to_power (n - 1)) * q <= q to_power n; then QA: (2 to_power (n - 1)) * q <= q |^ n; 2 to_power (n - 1) > 0 by POWER:34; then (2 to_power (n - 1)) * q > 0 by B1; then 1 / ((2 to_power (n-1)) * q) >= 1 / (q |^ n) by XREAL_1:118,QA; then |. x - p / q .| >= 1 / (q |^ n) by XXREAL_0:2,HG; hence thesis by B1; 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 proof deffunc G(Nat,Element of REAL) = In (a to_power (-(\$1+1)!),REAL); deffunc A() = In(0,REAL); consider f being sequence of REAL such that A1: f.0 = A() & for n being Nat holds f.(n+1) = G(n,f.n) from NAT_1:sch 12; reconsider f as Real_Sequence; take f; thus f.0 = 0 by A1; let n be non zero Nat; consider k being Nat such that A2: k + 1 = n by NAT_1:6; f.(k+1) = In(a to_power (-(k + 1)!), REAL) by A1 .= a to_power (-(k + 1)!); hence thesis by A2; end; uniqueness proof let f1,f2 be Real_Sequence; assume that A1: f1.0 = 0 & for n being non zero Nat holds f1.n = a to_power (-n!) and A2: f2.0 = 0 & for n being non zero Nat holds f2.n = a to_power (-n!); for n being Element of NAT holds f1.n = f2.n proof let n be Element of NAT; per cases; suppose n = 0; hence thesis by A1,A2; end; suppose A3: n <> 0; then f1.n = a to_power (-n!) by A1 .= f2.n by A2,A3; hence thesis; end; end; hence thesis by FUNCT_2:63; end; 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; ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: begin :: Other stuff, not really needed definition let b be Nat; func BLiouville_seq b -> Real_Sequence means :LiuSeq: for n being Nat holds it.n = b to_power (n!); correctness proof deffunc F(Nat) = b to_power (\$1!); thus (ex f being Real_Sequence st for n being Nat holds f.n = F(n)) & for f1, f2 being Real_Sequence st (for n being Nat holds f1.n = F(n)) & (for n being Nat holds f2.n = F(n)) holds f1 = f2 from IRRAT_1:sch 1; end; end; registration let b be Nat; cluster BLiouville_seq b -> NAT-valued; coherence proof set f = BLiouville_seq b; rng f c= NAT proof let x be object; assume x in rng f; then consider n being object such that AB: n in dom f & x = f.n by FUNCT_1:def 3; reconsider n as Nat by AB; AA: b to_power (n!) in INT by INT_1:def 2; f.n = b to_power (n!) by LiuSeq; hence thesis by AB; end; hence thesis by RELAT_1:def 19; end; end; registration cluster NAT-valued for Real_Sequence; existence proof take BLiouville_seq 1; thus thesis; end; end; definition let a be Real_Sequence; let b be Nat; :: assume b >= 2; func Liouville_seq (a,b) -> Real_Sequence means :DefLio: it.0 = 0 & for k being non zero Nat holds it.k = (a.k) / (b to_power (k!)); existence proof deffunc G(Nat,Element of REAL) = In ((a.(\$1 + 1)) / (b to_power ((\$1 + 1)!)),REAL); deffunc A() = In(0,REAL); consider f being sequence of REAL such that A1: f.0 = A() & for n being Nat holds f.(n+1) = G(n,f.n) from NAT_1:sch 12; reconsider f as Real_Sequence; take f; thus f.0 = 0 by A1; let n be non zero Nat; consider k being Nat such that A2: k + 1 = n by NAT_1:6; f.(k+1) = G(k,f.k) by A1 .= In((a.(k+1)) / (b to_power ((k + 1)!)), REAL) .= (a.(k + 1)) / (b to_power ((k + 1)!)); then f.n = (a.n) / (b to_power (n!)) by A2; hence thesis; end; uniqueness proof let f1,f2 be Real_Sequence; assume that A1: f1.0 = 0 & for n being non zero Nat holds f1.n = (a.n) / (b to_power (n!)) and A2: f2.0 = 0 & for n being non zero Nat holds f2.n = (a.n) / (b to_power (n!)); for n being Element of NAT holds f1.n = f2.n proof let n be Element of NAT; per cases; suppose n = 0; hence thesis by A1,A2; end; suppose A3: n <> 0; then f1.n = (a.n) / (b to_power (n!)) by A1 .= f2.n by A2,A3; hence thesis; end; end; hence thesis by FUNCT_2:63; end; end; definition let a be Real_Sequence; let b be Nat; func Liouville_constant (a,b) -> Real equals Sum Liouville_seq (a,b); coherence; end; registration let a be NAT-valued Real_Sequence; let b be non zero Nat; cluster Liouville_constant (a,b) -> liouville; coherence; ::> *4 end; theorem for n being Nat holds n * (n!) = (n + 1)! - n! proof let n be Nat; set a = n!; thus n * a = (n + 1) * a - a .= (n + 1)! - a by NEWTON:15; end; registration let a be Integer; let b be Nat; cluster a to_power b -> integer; coherence proof per cases; suppose a >= 0; then a in NAT by INT_1:3; then reconsider aa = a as Nat; aa to_power b is Integer; hence thesis; end; suppose a < 0; then -a >= 0; then reconsider aa = -a as Element of NAT by INT_1:3; per cases; suppose b is odd; then (-aa) |^ b = -(aa |^ b) by POWER:2; hence thesis; end; suppose b is even; then (-aa) |^ b = aa |^ b by POWER:1; hence thesis; end; end; end; end; theorem SomeLemma: for b being Nat st b > 1 holds |. 1 / b .| < 1 proof let b be Nat; assume A0: b > 1; then A1: b > 0; A2: 1 / b < 1 / 1 by A0,XREAL_1:76; |. 1 / b .| < 1 by A2; hence thesis; end; theorem for b being Nat st b > 1 holds Sum ((1/b) GeoSeq) = b / (b - 1) proof let b be Nat; assume A0: b > 1; then A2: b > 0; A1: |. 1 / b .| < 1 by SomeLemma,A0; then (1 / b) GeoSeq is summable by SERIES_1:24; Sum ((1/b) GeoSeq) = 1 / (1 - (1 / b)) by A1,SERIES_1:24 .= 1 / ((b / b) - (1 / b)) by XCMPLX_1:60,A2 .= 1 / ((b - 1) / b) by XCMPLX_1:120 .= b / (b - 1) by XCMPLX_1:57; hence thesis; end; registration let n be Nat; cluster seq_const n -> NAT-valued; coherence proof n in NAT by ORDINAL1:def 12; then seq_const n is Function of NAT, NAT by FUNCOP_1:46; then rng seq_const n c= NAT by RELAT_1:def 19; hence thesis by RELAT_1:def 19; end; end; registration cluster INT-valued for Real_Sequence; existence proof take f = seq_const 0; thus thesis; end; end; ::> ::> 4: This inference is not accepted