:: Introduction to {D}iophantine Approximation :: by Yasushige Watase :: :: Received April 19, 2015 :: Copyright (c) 2015-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 ARYTM_1, ARYTM_3, CARD_1, COMPLEX1, FINANCE1, FINSEQ_1, FUNCT_1, INT_1, IRRAT_1, NAT_1, NEWTON, NUMBERS, PROB_1, PROB_3, RAT_1, REAL_1, REAL_3, RELAT_1, SUBSET_1, TARSKI, XBOOLE_0, XXREAL_0, XXREAL_1, INT_2, ORDINAL1, SQUARE_1, ABIAN, FINSET_1, SEQ_1, ORDINAL2, SEQ_2, VALUED_1, DIOPHAN1, NAT_6; notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, XREAL_0, COMPLEX1, FINSEQ_1, XXREAL_1, PROB_1, FINANCE1, PROB_3, IRRAT_1, REAL_3, NEWTON, SQUARE_1, REAL_1, ABIAN, INT_2, FINSET_1, RAT_1, COMSEQ_2, SEQ_1, SEQ_2, VALUED_1, NAT_D, FUNCOP_1, NAT_6; constructors REAL_1, SQUARE_1, SEQ_2, NEWTON, RELSET_1, COMSEQ_2, ABIAN, REAL_3, PROB_3, FINANCE1, NAT_6; registrations XREAL_0, NAT_1, INT_1, FINSET_1, XXREAL_0, NEWTON, CARD_1, VALUED_0, RELSET_1, NUMBERS, XCMPLX_0, FUNCT_2, ABIAN, NAT_3, SQUARE_1, REAL_3, ZFMISC_1, FINANCE1, RAT_1, MEMBERED, VALUED_1, SEQ_1, SEQ_2, NAT_6; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions NAT_6; equalities ORDINAL1, FINSEQ_1, SUBSET_1, CARD_3, XBOOLE_0, CARD_1, VALUED_1, XCMPLX_0; expansions TARSKI, XBOOLE_0, PBOOLE, XREAL_0, SETFAM_1, ORDINAL1, NAT_6, FUNCT_1; theorems AXIOMS, INT_1, INT_2, NAT_1, XXREAL_0, XREAL_1, FINSEQ_1, ORDINAL1, XBOOLE_1, FUNCT_1, FUNCT_2, ABSVALUE, NEWTON, XXREAL_1, CARD_1, FINSEQ_4, COMPLEX1, XCMPLX_0, XCMPLX_1, PROB_3, CARD_2, REAL_3, SERIES_2, SQUARE_1, WSIERP_1, RAT_1, SEQ_1, VALUED_1, SEQ_2; schemes FUNCT_2, FINSEQ_1, NAT_1, FIB_NUM, SEQ_1; begin :: Irrational & Continued Fraction reserve i,j,k,m,n,m1,n1 for Nat; reserve a,r,r1,r2 for Real; reserve m0,cn,cd for Integer; reserve x1,x2,o for object; :: Approximation an irrational by its simple continued fraction theorem Th1: r = rfs(r).0 & r = scf(r).0 + 1/rfs(r).1 & rfs(r).n = scf(r).n + 1/rfs(r).(n+1) proof A1: rfs(r).1 = rfs(r).(0+1) .= 1/frac(rfs(r).0) by REAL_3:def 3; A2: frac(rfs(r).0) = frac(r) by REAL_3:def 3 .= r - scf(r).0 by REAL_3:35; A4: frac(rfs(r).n) = rfs(r).n - [\ rfs(r).n /] by INT_1:def 8; 1/rfs(r).(n+1) = 1/(1/frac(rfs(r).n)) by REAL_3:def 3 .= frac(rfs(r).n); then scf(r).n + 1/rfs(r).(n+1) = scf(r).n + rfs(r).n - [\ rfs(r).n /] by A4 .= scf(r).n + rfs(r).n - scf(r).n by REAL_3:def 4 .= rfs(r).n; hence thesis by REAL_3:def 3,A2,A1; end; theorem Th2: r is irrational implies rfs(r).n is irrational proof assume A1: r is irrational; set rn = rfs(r).n; A3: scf(rn).0 = [\ rfs(rn).0 /] by REAL_3:def 4 .= [\ rfs(r).n /] by REAL_3:def 3 .= scf(r).n by REAL_3:def 4; A4: scf(rn).m = scf(r).(n+m) & rfs(rn).m = rfs(r).(n+m) proof defpred P[Nat] means scf(rn).\$1 = scf(r).(n+\$1) & rfs(rn).\$1 = rfs(r).(n+\$1); A5: P[0] by REAL_3:def 3,A3; A6: for m be Nat st P[m] holds P[m+1] proof let m be Nat; assume A7: P[m]; A9: rfs(rn).(m+1) = 1 / frac(rfs(rn).m) by REAL_3:def 3 .= rfs(r).(n+m+1) by A7,REAL_3:def 3; scf(rn).(m+1)= [\ rfs(rn).(m+1) /] by REAL_3:def 4 .= scf(r).(n+m+1) by A9,REAL_3:def 4; hence thesis by A9; end; for m be Nat holds P[m] from NAT_1:sch 2(A5,A6); hence thesis; end; assume A10:rfs(r).n is rational; consider n1 such that A12:for m1 st m1 >= n1 holds scf(rn).m1 = 0 by A10,REAL_3:42; A13:for m1 st m1 >= n1 holds scf(r).(n+m1) = 0 proof let m1; assume A14: m1 >= n1; scf(r).(n+m1)=scf(rn).m1 by A4 .= 0 by A12,A14; hence thesis; end; for m st m >= n1+n holds scf(r).m = 0 proof let m; assume A15: m >= n1+n; A16: m -n >= n1+n - n by A15,XREAL_1:9; m - n in NAT by A16,INT_1:3; then reconsider l = m - n as Nat; scf(r).(n+l) = 0 by A13,A16; hence thesis; end; hence contradiction by A1,REAL_3:42; end; theorem Th3: r is irrational implies rfs(r).n <> 0 & rfs(r).1*rfs(r).2 <> 0 & scf(r).1*rfs(r).2 + 1 <> 0 proof assume A1: r is irrational; A2: rfs(r).n <> 0 proof assume rfs(r).n = 0; then consider n1 be Nat such that A4: rfs(r).n1 = 0; n1 <= m implies scf(r).m = 0 by A4,REAL_3:28; hence contradiction by A1,REAL_3:42; end; A5: rfs(r).1 <> 0 & rfs(r).2 <> 0 by A1,Th2; rfs(r).1 = scf(r).1 + 1/rfs(r).(1+1) by Th1; then rfs(r).1*rfs(r).2 = scf(r).1*rfs(r).2 + (1/rfs(r).2)*rfs(r).2 .= scf(r).1*rfs(r).2 + 1 by XCMPLX_1:106,A5; hence thesis by A2,A5; end; theorem Th4: r is irrational implies scf(r).n < rfs(r).n & rfs(r).n < scf(r).n + 1 & 1 < rfs(r).(n+1) proof assume r is irrational; then A2: rfs(r).n is not integer by Th2; A3: 1/rfs(r).(n+1) = 1/(1/frac(rfs(r).n)) by REAL_3:def 3 .= frac(rfs(r).n); A4: 1/rfs(r).(n +1)> 0 by A2,A3,INT_1:46; A5: rfs(r).n = scf(r).n + 1/rfs(r).(n+1) by Th1; A6: rfs(r).n - scf(r).n + scf(r).n > 0 + scf(r).n by A2,A3,A5,INT_1:46,XREAL_1:8; 1" < ((rfs(r).(n +1))")" by A3,INT_1:43,A4,XREAL_1:88; hence thesis by A6,A5,A3,INT_1:43,XREAL_1:8; end; theorem Th5: r is irrational implies 0 < scf(r).(n+1) proof assume A1: r is irrational; A2: rfs(r).(n +1)-1 > 1-1 by A1,Th4,XREAL_1:14; rfs(r).(n +1) < scf(r).(n +1) + 1 by A1,Th4; then rfs(r).(n +1) -1 < scf(r).(n +1) + 1 -1 by XREAL_1:14; hence thesis by A2; end; Th6: for n holds c_n(r).n is Integer proof defpred P[Nat] means c_n(r).\$1 is Integer; A1: for n being Nat st P[n] & P[n+1] holds P[n+2] proof let n be Nat; assume that A2: c_n(r).n is Integer and A3: c_n(r).(n+1) is Integer; c_n(r).(n+2) = scf(r).(n+2) * c_n(r).(n+1) + c_n(r).n by REAL_3:def 5; hence thesis by A2,A3; end; A5: P[1] proof c_n(r).1 = scf(r).1 * scf(r).0 + 1 by REAL_3:def 5; hence thesis; end; A6: P[0] proof c_n(r).0 = scf(r).0 by REAL_3:def 5; hence thesis; end; for n being Nat holds P[n] from FIB_NUM:sch 1(A6,A5,A1); hence thesis; end; registration let r,n; cluster c_n(r).n -> integer; coherence by Th6; end; theorem Th7: :: [Hardy&Wright] Ch.10 Th155 r is irrational implies for n holds c_d(r).(n+1) >= c_d(r).n proof assume A1: r is irrational; defpred P[Nat] means c_d(r).\$1 <= c_d(r).(\$1+1); A2: P[0] proof A3: c_d(r).0 = 1 by REAL_3:def 6; rfs(r).(0+1) > 1 by A1,Th4; then rfs(r).1 - 1 > 1 -1 by XREAL_1:14; then [\ rfs(r).1 /] > 0 by INT_1:def 6; then scf(r).1 > 0 by REAL_3:def 4; then 0+1 <= scf(r).1 by INT_1:7; hence thesis by A3,REAL_3:def 6; end; A8: for n be Nat st P[n] holds P[n+1] proof let n be Nat; assume P[n]; A9: c_d(r).(n+2) - c_d(r).(n+1) = scf(r).(n+2) * c_d(r).(n+1) + c_d(r).n - c_d(r).(n+1) by REAL_3:def 6 .= (scf(r).(n+2) -1) * c_d(r).(n+1) + c_d(r).n; A10: scf(r).(n+2) = [\ rfs(r).(n+2) /] by REAL_3:def 4; rfs(r).(n+1+1) > 1 by A1,Th4; then rfs(r).(n+2) - 1 > 1 -1 by XREAL_1:14; then scf(r).(n+2) > 0 by A10,INT_1:def 6; then 0+1 <= scf(r).(n+2) by INT_1:7; then A12: scf(r).(n+2) -1 >= 1 -1 by XREAL_1:13; c_d(r).(n+1) >= 0 & c_d(r).n >= 0 by REAL_3:51; then c_d(r).(n+2) - c_d(r).(n+1) + c_d(r).(n+1) >= 0 + c_d(r).(n+1) by A9,A12,XREAL_1:6; hence thesis; end; for n be Nat holds P[n] from NAT_1:sch 2(A2,A8); hence thesis; end; theorem Th8: r is irrational implies c_d(r).n >=1 proof assume A1: r is irrational; defpred P[Nat] means c_d(r).\$1 >=1; A2: P[0] by REAL_3:def 6; A3: for n be Nat st P[n] holds P[n+1] proof let n be Nat; assume A4: P[n]; c_d(r).(n+1) >= c_d(r).n by A1,Th7; hence thesis by A4,XXREAL_0:2; end; for n be Nat holds P[n] from NAT_1:sch 2(A2,A3); hence thesis; end; ::[Hardy&Wright] Irrational case of Ch. 10 Th155 theorem r is irrational implies c_d(r).(n+2) > c_d(r).(n+1) proof assume A1: r is irrational; then A2: scf(r).(n+1+1) > 0 by Th5; A3: n+2 >= 0+1 by XREAL_1:8; A4: c_d(r).(n+2) = scf(r).(n+2) * c_d(r).(n+1) + c_d(r).n by REAL_3:def 6; c_d(r).n > 0 by A1,Th8; then A5: c_d(r).(n+2) -0 > scf(r).(n+2) * c_d(r).(n+1) + c_d(r).n - c_d(r).n by A4,XREAL_1:15; c_d(r).(n+1) >= 1 by A1,Th8; then scf(r).(n+2)*c_d(r).(n+1) >= c_d(r).(n+1) by A2,A3,REAL_3:40,XREAL_1:151; hence thesis by A5,XXREAL_0:2; end; ::[Hardy&Wright] Ch.10 Th156 theorem Th10: r is irrational implies c_d(r).n >= n proof assume A1: r is irrational; defpred P[Nat] means c_d(r).\$1 >= \$1; A2: P[0] by REAL_3:def 6; A3: for n be Nat st P[n] holds P[n+1] proof let n be Nat; assume A4: P[n]; set m = n -1; per cases; suppose n=0; hence thesis by A1,Th8; end; suppose n > 0; then reconsider m as Nat; A7: scf(r).(m+1+1) > 0 by A1,Th5; A8: m+2 >= 0+1 by XREAL_1:8; c_d(r).(m+1) >= 1 by A1,Th8; then A9: scf(r).(m+2)*c_d(r).(m+1) >= c_d(r).(m+1) by A7,A8,REAL_3:40,XREAL_1:151; scf(r).(m+2)*c_d(r).(m+1) + c_d(r).m >= c_d(r).(m+1) +c_d(r).m by A9,XREAL_1:6; then A12: c_d(r).(m+2) >= c_d(r).(m+1) + c_d(r).m by REAL_3:def 6; A13: c_d(r).(m+1) + c_d(r).m >= n+c_d(r).m by A4,XREAL_1:6; n+c_d(r).m >= n + 1 by A1,Th8,XREAL_1:6; then c_d(r).(m+1) + c_d(r).m >= n + 1 by A13,XXREAL_0:2; hence thesis by A12,XXREAL_0:2; end; end; for n be Nat holds P[n] from NAT_1:sch 2(A2,A3); hence thesis; end; ::[Hardy&Wright] Ch.10 Th157 theorem cn = c_n(r).n & cd = c_d(r).n & cn <> 0 implies cn,cd are_coprime proof c_d(r).(n+1) in NAT by REAL_3:50; then reconsider cd2 = c_d(r).(n+1) as Integer; reconsider cn2 = c_n(r).(n+1) as Integer; assume that A2: cn = c_n(r).n and A3: cd = c_d(r).n and A4: cn <> 0; assume A5: not (cn,cd are_coprime); A6: cn2*cd -cn*cd2 = (-1)|^n by A2,A3,REAL_3:64; consider cn0,cd0 be Integer such that A8: cn = (cn gcd cd)*cn0 and A9: cd = (cn gcd cd)*cd0 and cn0,cd0 are_coprime by A4,INT_2:23; cn gcd cd <> 0 by A4,INT_2:5; then cn gcd cd >= 0 +1 by INT_1:7; then A11:cn gcd cd > 1 by A5,INT_2:def 3,XXREAL_0:1; A12:(-1)|^n = cn2*(cn gcd cd)*cd0 -cn*cd2 by A6,A9 .= (cn gcd cd)*(cn2*cd0 - cn0*cd2) by A8; A13:1=|.(-1)|^n.| by SERIES_2:1 .=|.(cn gcd cd)*(cn2*cd0-cn0*cd2).| by A12 .=|.(cn gcd cd).|*|.(cn2*cd0-cn0*cd2).| by COMPLEX1:65 .=(cn gcd cd)*|.(cn2*cd0-cn0*cd2).| by ABSVALUE:def 1; (cn gcd cd)" < 1 by A11,XREAL_1:212; then |.(cn2*cd0-cn0*cd2).| < 1 by A13,XCMPLX_1:210; then |.(cn2*cd0-cn0*cd2).| = 0 by NAT_1:14; hence contradiction by A13; end; theorem Th12: r is irrational implies (c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n) > 0 & (c_d(r).(n+1)*rfs(r).(n+2) - c_d(r).n) > 0 proof assume A1: r is irrational; then A2: c_d(r).(n+1) >= 1 by Th8; rfs(r).(n+1+1) > 1 by A1,Th4; then A4: rfs(r).(n+2)*c_d(r).(n+1) > 1*c_d(r).(n+1) by A2,XREAL_1:68; then A5: c_d(r).(n+1)*rfs(r).(n+2) > 1 by A2,XXREAL_0:2; A6: c_d(r).n + 1 >= 1 + 1 by A1,Th8,XREAL_1:6; c_d(r).(n+1) >= c_d(r).n by A1,Th7; then c_d(r).(n+1)*rfs(r).(n+2) > c_d(r).n by A4,XXREAL_0:2; then c_d(r).(n+1)*rfs(r).(n+2)-c_d(r).n > c_d(r).n-c_d(r).n by XREAL_1:14; hence thesis by A5,A6,XREAL_1:6; end; theorem Th13: r is irrational implies (c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n)) > 0 proof assume A1: r is irrational; then A2: c_d(r).(n+1) >=1 by Th8; (c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n) > 0 by A1,Th12; hence thesis by A2; end; theorem Th14: r is irrational implies r = (c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n)/ (c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n) proof assume A1: r is irrational; defpred P[Nat] means r = (c_n(r).(\$1+1)*rfs(r).(\$1+2)+c_n(r).\$1) /(c_d(r).(\$1+1)*rfs(r).(\$1+2)+c_d(r).\$1); A2: P[0] proof A3: rfs(r).1 = scf(r).1 + 1/rfs(r).(1+1) by Th1; A4: (c_n(r).1*rfs(r).2+c_n(r).0) = (scf(r).1 * scf(r).0 + 1) *rfs(r).2+c_n(r).0 by REAL_3:def 5 .= (scf(r).1 * scf(r).0 + 1) *rfs(r).2 + scf(r).0 by REAL_3:def 5 .= scf(r).0*(scf(r).1 *rfs(r).2 + 1) + rfs(r).2; A5: (c_d(r).1*rfs(r).2+c_d(r).0)=scf(r).1*rfs(r).2+c_d(r).0 by REAL_3:def 6 .= scf(r).1*rfs(r).2 + 1 by REAL_3:def 6; A6: rfs(r).2 <> 0 & scf(r).1*rfs(r).2 + 1 <> 0 by A1,Th3; (c_n(r).1*rfs(r).2+c_n(r).0)/(c_d(r).1*rfs(r).2+c_d(r).0)= (scf(r).0*(scf(r).1*rfs(r).2+1)+rfs(r).2)/(c_d(r).1*rfs(r).2+c_d(r).0) by A4 .= scf(r).0*((scf(r).1 *rfs(r).2 + 1)/( (scf(r).1*rfs(r).2 + 1))) + rfs(r).2 /(scf(r).1*rfs(r).2 + 1) by A5 .= scf(r).0 *1 + rfs(r).2 /(scf(r).1*rfs(r).2 + 1) by A6,XCMPLX_1:60 .= scf(r).0+(rfs(r).2/rfs(r).2)/((scf(r).1*rfs(r).2+1)/rfs(r).2) by A6,XCMPLX_1:55 .= scf(r).0+1/((scf(r).1*rfs(r).2+1)/rfs(r).2) by A6,XCMPLX_1:60 .= scf(r).0 + 1/(scf(r).1*(rfs(r).2/rfs(r).2)+1/rfs(r).2) .= scf(r).0 + 1/(scf(r).1*1+1/rfs(r).2) by A1,Th3,XCMPLX_1:60 .= r by Th1,A3; hence thesis; end; A7: for n be Nat st P[n] holds P[n+1] proof let n be Nat; assume A8: P[n]; A9: rfs(r).(n+2) = scf(r).(n+2) + 1/rfs(r).(n+2 +1) by Th1 .= scf(r).(n+2) + 1/rfs(r).(n+3); A10: 1 = (rfs(r).(n+3))/(rfs(r).(n+3)) by A1,Th3,XCMPLX_1:60; A11: c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n = c_n(r).(n+1)*(scf(r).(n+2) + 1/rfs(r).(n+3))+c_n(r).n by A9 .= scf(r).(n+2) * c_n(r).(n+1) + c_n(r).n + c_n(r).(n+1)* (1/rfs(r).(n+3)) .= c_n(r).(n+2) + c_n(r).(n+1)* (1/rfs(r).(n+3)) by REAL_3:def 5; A12: c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n = c_d(r).(n+1)*(scf(r).(n+2) + 1/rfs(r).(n+3))+c_d(r).n by A9 .= scf(r).(n+2) * c_d(r).(n+1) + c_d(r).n + c_d(r).(n+1)* (1/rfs(r).(n+3)) .= c_d(r).(n+2) + c_d(r).(n+1)* (1/rfs(r).(n+3)) by REAL_3:def 6; r=(c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n)/(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n) by A8 .= (c_n(r).(n+2) + c_n(r).(n+1)* (1/rfs(r).(n+3)))/ (c_d(r).(n+2) + c_d(r).(n+1)* (1/rfs(r).(n+3))) by A11,A12 .= ((c_n(r).(n+2) + c_n(r).(n+1)* (1/rfs(r).(n+3))) /(c_d(r).(n+2) + c_d(r).(n+1)* (1/rfs(r).(n+3)))) *(rfs(r).(n+3)/rfs(r).(n+3)) by A10 .= ((c_n(r).(n+2) + c_n(r).(n+1)* (1/rfs(r).(n+3))) * rfs(r).(n+3)) /((c_d(r).(n+2) + c_d(r).(n+1)* (1/rfs(r).(n+3))) * rfs(r).(n+3)) by XCMPLX_1:76 .= ((c_n(r).(n+2)*rfs(r).(n+3) +c_n(r).(n+1)* ((1/rfs(r).(n+3))*rfs(r).(n+3)) )) /((c_d(r).(n+2)*rfs(r).(n+3) +c_d(r).(n+1)* ((1/rfs(r).(n+3))*rfs(r).(n+3)) )) .= ((c_n(r).(n+2)*rfs(r).(n+3) +c_n(r).(n+1)*1)) /((c_d(r).(n+2)*rfs(r).(n+3) +c_d(r).(n+1)*((1/rfs(r).(n+3))*rfs(r).(n+3)) )) by XCMPLX_1:106,A1,Th3 .= ((c_n(r).(n+2)*rfs(r).(n+3) +c_n(r).(n+1)*1)) /((c_d(r).(n+2)*rfs(r).(n+3) +c_d(r).(n+1)*1)) by XCMPLX_1:106,A1,Th3 .= (c_n(r).(n+1+1)*rfs(r).(n+1+2) +c_n(r).(n+1)) /(c_d(r).(n+1+1)*rfs(r).(n+1+2) +c_d(r).(n+1)); hence thesis; end; for n be Nat holds P[n] from NAT_1:sch 2(A2,A7); hence thesis; end; ::[Hardy&Wright] Ch.10 Th158 theorem Th15: r is irrational implies c_n(r).(n+1)/c_d(r).(n+1) - r = (-1)|^n /(c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n)) proof assume A1: r is irrational; then A3: c_d(r).(n+1) <> 0 by Th8; A4: c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n <> 0 by A1,Th12; A5: c_n(r).(n+1)/c_d(r).(n+1) - r = c_n(r).(n+1)/c_d(r).(n+1) - (c_n(r).(n+1)*rfs(r).(n+2) + c_n(r).n) /(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n) by A1,Th14 .= (c_n(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n) - (c_n(r).(n+1)*rfs(r).(n+2) + c_n(r).n)*c_d(r).(n+1) ) /(c_d(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n)) by A3,A4,XCMPLX_1:130; (c_n(r).(n+1)*(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n) - (c_n(r).(n+1)*rfs(r).(n+2) + c_n(r).n)*c_d(r).(n+1)) = c_n(r).(n+1)*c_d(r).(n+1)*rfs(r).(n+2) + c_n(r).(n+1)*c_d(r).n - c_n(r).(n+1)*c_d(r).(n+1)*rfs(r).(n+2) - c_n(r).n*c_d(r).(n+1) .= (-1)|^n by REAL_3:64; hence thesis by A5; end; theorem Th16: r is irrational & n is even & n > 0 implies r > c_n(r).n/c_d(r).n proof assume A1: r is irrational; assume A2: n is even; assume n > 0; then reconsider m = n -1 as odd natural number by A2; (c_d(r).(m+1)*(c_d(r).(m+1)*rfs(r).(m+2) + c_d(r).m)) > 0 by A1,Th13; then (-1)|^m /(c_d(r).(m+1)*(c_d(r).(m+1)*rfs(r).(m+2) + c_d(r).m)) < 0; then c_n(r).(m+1)/c_d(r).(m+1) - r < 0 by A1,Th15; then c_n(r).(n-1+1)/c_d(r).(n-1+1) -r + r < 0 + r by XREAL_1:8; hence thesis; end; theorem Th17: r is irrational & n is odd implies r < c_n(r).n/c_d(r).n proof assume A1: r is irrational; assume n is odd; then reconsider m = n -1 as even natural number; (c_d(r).(m+1)*(c_d(r).(m+1)*rfs(r).(m+2) + c_d(r).m)) > 0 by A1,Th13; then (-1)|^m /(c_d(r).(m+1)*(c_d(r).(m+1)*rfs(r).(m+2) + c_d(r).m)) > 0; then c_n(r).(m+1)/c_d(r).(m+1) - r > 0 by A1,Th15; then c_n(r).(m+1)/c_d(r).(m+1) - r + r > 0 + r by XREAL_1:8; hence thesis; end; theorem r is irrational & n > 0 implies |. r - c_n(r).n/c_d(r).n .| + |. r - c_n(r).(n+1)/c_d(r).(n+1) .| = |. c_n(r).n/c_d(r).n - c_n(r).(n+1)/c_d(r).(n+1) .| proof assume that A1: r is irrational and A2: n > 0; per cases; suppose A3: n is even; r > c_n(r).n/c_d(r).n by A1,A2,A3,Th16; then A4: r - c_n(r).n/c_d(r).n > c_n(r).n/c_d(r).n - c_n(r).n/c_d(r).n by XREAL_1:14; r - c_n(r).n/c_d(r).n <> 0 by A1,A2,A3,Th16; then |. r - c_n(r).n/c_d(r).n.| <> 0 by ABSVALUE:2; then A5: |. r - c_n(r).n/c_d(r).n .| > 0 by COMPLEX1:46; A8: r - c_n(r).(n+1)/c_d(r).(n+1) < c_n(r).(n+1)/c_d(r).(n+1) -c_n(r).(n+1)/c_d(r).(n+1) by A1,A3,Th17,XREAL_1:14;then |. r - c_n(r).(n+1)/c_d(r).(n+1).| <> 0 by ABSVALUE:2; then A9: |. r - c_n(r).(n+1)/c_d(r).(n+1) .| > 0 by COMPLEX1:46; A10: |. r - c_n(r).n/c_d(r).n .| + |. r - c_n(r).(n+1)/c_d(r).(n+1) .| = r - c_n(r).n/c_d(r).n + |. r - c_n(r).(n+1)/c_d(r).(n+1) .| by A4,ABSVALUE:def 1 .= r - c_n(r).n/c_d(r).n + -(r - c_n(r).(n+1)/c_d(r).(n+1)) by A8,ABSVALUE:def 1 .= - (c_n(r).n/c_d(r).n - c_n(r).(n+1)/c_d(r).(n+1)); c_n(r).n/c_d(r).n - c_n(r).(n+1)/c_d(r).(n+1) < 0 by A5,A9,A10; hence thesis by A10,ABSVALUE:def 1; end; suppose A11: n is odd; then A13: r - c_n(r).n/c_d(r).n < c_n(r).n/c_d(r).n - c_n(r).n/c_d(r).n by XREAL_1:14,A1,Th17; r - c_n(r).n/c_d(r).n <> 0 by A1,A11,Th17; then |. r - c_n(r).n/c_d(r).n.| <> 0 by ABSVALUE:2; then A14: |. r - c_n(r).n/c_d(r).n .| > 0 by COMPLEX1:46; r > c_n(r).(n+1)/c_d(r).(n+1) by A1,A11,Th16; then A18: r - c_n(r).(n+1)/c_d(r).(n+1) > c_n(r).(n+1)/c_d(r).(n+1)-c_n(r).(n+1)/c_d(r).(n+1) by XREAL_1:14; |. r - c_n(r).(n+1)/c_d(r).(n+1).| <> 0 by A18,ABSVALUE:2; then A19: |. r - c_n(r).(n+1)/c_d(r).(n+1) .| > 0 by COMPLEX1:46; |. r - c_n(r).n/c_d(r).n .| + |. r - c_n(r).(n+1)/c_d(r).(n+1) .| = -(r - c_n(r).n/c_d(r).n) + |. r - c_n(r).(n+1)/c_d(r).(n+1) .| by A13,ABSVALUE:def 1 .= -r + c_n(r).n/c_d(r).n + (r - c_n(r).(n+1)/c_d(r).(n+1)) by A18,ABSVALUE:def 1 .= c_n(r).n/c_d(r).n - c_n(r).(n+1)/c_d(r).(n+1); hence thesis by A14,A19,ABSVALUE:def 1; end; end; theorem Th19: r is irrational implies |. r - c_n(r).n/c_d(r).n .| > 0 proof assume A1: r is irrational; assume not |. r - c_n(r).n/c_d(r).n .| > 0; then |. r - c_n(r).n/c_d(r).n .| = 0 by COMPLEX1:46; then A3: r - c_n(r).n/c_d(r).n = 0 by COMPLEX1:45; c_d(r).n in NAT by REAL_3:50; hence contradiction by A1,A3; end; theorem r is irrational implies c_d(r).(n+2) >= 2*c_d(r).n proof assume A1: r is irrational; then scf(r).(n+1+1) > 0 by Th5; then A4: scf(r).(n+2) >=0+1 by INT_1:7; A5: 0 < c_d(r).n by A1,Th8; c_d(r).n <= c_d(r).(n+1) by A1,Th7; then scf(r).(n+2) * c_d(r).(n+1) >= 1*c_d(r).n by A4,A5,XREAL_1:66; then scf(r).(n+2)*c_d(r).(n+1) + c_d(r).n >= 1*c_d(r).n + c_d(r).n by XREAL_1:6; hence thesis by REAL_3:def 6; end; theorem Th21: r is irrational implies |. r - c_n(r).(n+1)/c_d(r).(n+1) .| < 1/(c_d(r).(n+1)*c_d(r).(n+2)) proof assume A1: r is irrational; then A2: c_d(r).(n+1) >= 1 by Th8; A3: c_d(r).(n+1+1) >= 1 by A1,Th8; scf(r).(n+2)*c_d(r).(n+1) < rfs(r).(n+2)*c_d(r).(n+1) by A1,Th4,A2,XREAL_1:68; then scf(r).(n+2)*c_d(r).(n+1)+c_d(r).n < rfs(r).(n+2)*c_d(r).(n+1)+c_d(r).n by XREAL_1:8; then A5: c_d(r).(n+2) 0 by A1,Th12; A4: r*c_d(r).(n+1)*rfs(r).(n+2) + r*c_d(r).n = (c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n) *((1/(c_d(r).(n+1)*rfs(r).(n+2)+c_d(r).n)) *(c_d(r).(n+1)*rfs(r).(n+2) + c_d(r).n)) by A2 .= (c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n) * 1 by A3,XCMPLX_1:106 .= c_n(r).(n+1)*rfs(r).(n+2)+c_n(r).n; A6: -(r*c_d(r).n - c_n(r).n) = r*c_d(r).(n+1)*rfs(r).(n+2) - c_n(r).(n+1)*rfs(r).(n+2) by A4 .= rfs(r).(n+2)*(r*c_d(r).(n+1) - c_n(r).(n+1)); A7: 1 < rfs(r).(n+1+1) by A1,Th4; A8: |. r*c_d(r).n-c_n(r).n .| = |.-(r*c_d(r).n-c_n(r).n).| by COMPLEX1:52 .= |. rfs(r).(n+2)*(r*c_d(r).(n+1) - c_n(r).(n+1)) .| by A6 .= |. rfs(r).(n+2) .|*|.(r*c_d(r).(n+1) - c_n(r).(n+1)) .| by COMPLEX1:65 .= rfs(r).(n+2) *|. r*c_d(r).(n+1) - c_n(r).(n+1) .| by A7,COMPLEX1:43; A9: c_d(r).(n+1) >= 1 & c_d(r).n >=1 by A1,Th8; |. r - c_n(r).(n+1)/c_d(r).(n+1) .| > 0 by A1,Th19; then A11: r-c_n(r).(n+1)/c_d(r).(n+1) <> 0 by COMPLEX1:47; A12: (r-c_n(r).(n+1)/c_d(r).(n+1)) * c_d(r).(n+1) = r*c_d(r).(n+1) - c_n(r).(n+1)/c_d(r).(n+1) * c_d(r).(n+1) .= r*c_d(r).(n+1) - c_n(r).(n+1) by A9,XCMPLX_1:87; then A13: |. r*c_d(r).n-c_n(r).n .| > |. r*c_d(r).(n+1) - c_n(r).(n+1) .| by A7,A8,A9,A11,COMPLEX1:47,XREAL_1:155; A14: |. r - c_n(r).(n+1)/c_d(r).(n+1) .| = |. r*c_d(r).(n+1)/c_d(r).(n+1)-c_n(r).(n+1)/c_d(r).(n+1) .| by A9,XCMPLX_1:89 .= |. (r*c_d(r).(n+1)-c_n(r).(n+1))/c_d(r).(n+1) .| .= |. (r*c_d(r).(n+1)-c_n(r).(n+1)).|/|.c_d(r).(n+1) .| by COMPLEX1:67 .= |. r*c_d(r).(n+1)-c_n(r).(n+1).|/c_d(r).(n+1) by A9,COMPLEX1:43; A15: |. r - c_n(r).n/c_d(r).n .| = |. r*c_d(r).n/c_d(r).n-c_n(r).n/c_d(r).n .| by A9,XCMPLX_1:89 .= |. (r*c_d(r).n-c_n(r).n)/c_d(r).n .| .= |. (r*c_d(r).n-c_n(r).n).|/|.c_d(r).n .| by COMPLEX1:67 .= |. r*c_d(r).n-c_n(r).n.|/c_d(r).n by A9,COMPLEX1:43; A16: |. r*c_d(r).(n+1)-c_n(r).(n+1).|/c_d(r).(n+1) < |. r*c_d(r).n - c_n(r).n .| / c_d(r).(n+1) by A9,A13,XREAL_1:74; |. r*c_d(r).n - c_n(r).n .| >= 0 by COMPLEX1:46; then |. r*c_d(r).n - c_n(r).n .| / c_d(r).(n+1) <= |. r*c_d(r).n - c_n(r).n .| / c_d(r).n by A1,Th7,A9,XREAL_1:118; hence thesis by A7,A8,A9,A11,A12,A14,A15,A16,COMPLEX1:47, XREAL_1:155,XXREAL_0:2; end; theorem Th23: r is irrational & m > n implies |. r - c_n(r).n/c_d(r).n .| > |. r - c_n(r).m/c_d(r).m .| proof assume that A1: r is irrational and A3: m > n; defpred P[Nat] means |. r - c_n(r).n/c_d(r).n .| > |. r - c_n(r).(n+1+\$1)/c_d(r).(n+1+\$1) .|; A4: P[0] by A1,Th22; A5: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume P[k]; then |.r-c_n(r).n/c_d(r).n.| > |.r-c_n(r).(n+1+k+1)/c_d(r).(n+1+k+1).| by A1,Th22,XXREAL_0:2; hence thesis; end; A8: for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); m - n > n-n by A3,XREAL_1:14; then m - n >= 0+1 by INT_1:7; then A9: (m - n) - 1 >= 1 - 1 by XREAL_1:9; reconsider i = m - n - 1 as Integer; i in NAT by A9,INT_1:3; then reconsider i as Nat; |. r - c_n(r).n/c_d(r).n .| > |. r - c_n(r).(n+1+i)/c_d(r).(n+1+i) .| by A8; hence thesis; end; ::[Hardy&Wright] Ch.10 Th164 theorem Th24: r is irrational implies |. r - c_n(r).n/c_d(r).n .| < 1/c_d(r).n|^2 proof assume A1: r is irrational; |. r - c_n(r).n/c_d(r).n .| < 1/c_d(r).n|^2 proof per cases; suppose A3: n = 0; then A6: |. r - c_n(r).n/c_d(r).n .| = |. r - c_n(r).0/1 .| by REAL_3:def 6 .= |. r - scf(r).0 .| by REAL_3:def 5 .= |.r-[\ rfs(r).0 /].| by REAL_3:def 4 .= |.r-[\ r /].| by REAL_3:def 3 .= |. frac r .| by INT_1:def 8 .= frac r by ABSVALUE:def 1,INT_1:43; 1/c_d(r).n|^2 = 1/c_d(r).0|^2 by A3 .= 1/1|^2 by REAL_3:def 6 .= 1; hence thesis by A6,INT_1:43; end; suppose A8: n > 0; set m = n - 1; reconsider m as Nat by A8; A10: c_d(r).(m+1) >= 1 by A1,Th8; then c_d(r).(m+1)*c_d(r).(m+1) >= 1 by XREAL_1:159; then A12: c_d(r).(m+1)|^2 >=1 by WSIERP_1:1; c_d(r).(m+1+1)*c_d(r).(m+1)>=c_d(r).(m+1)*c_d(r).(m+1) by A1,A10,Th7,XREAL_1:64; then c_d(r).(m+1)*c_d(r).(m+2)>=c_d(r).(m+1)|^2 by WSIERP_1:1; then 1/(c_d(r).(m+1)*c_d(r).(m+2)) <= 1/c_d(r).(m+1)|^2 by A12,XREAL_1:85; hence thesis by A1,XXREAL_0:2,Th21; end; end; hence thesis; end; theorem for S be Subset of RAT, r st r is irrational & S = {p where p is Element of RAT: |. r - p .| < 1/denominator(p)|^2 } holds S is infinite proof let S be Subset of RAT, r; assume that A1: r is irrational and A2: S = {p where p is Element of RAT: |. r - p .| < 1/denominator(p)|^2 }; deffunc F(Nat) = c_n(r).(\$1 +1)/c_d(r).(\$1 +1); consider f being Real_Sequence such that A3: for n being Nat holds f.n = F(n) from SEQ_1:sch 1; for o be Real st o in rng f holds o in S proof let o be Real; assume o in rng f; then consider i being object such that A6: i in dom f and A7: o = f.i by FUNCT_1:def 3; reconsider i as Nat by A6; A8: o = F(i) by A7,A3 .= c_n(r).(i+1)/c_d(r).(i +1); A9: c_d(r).(i+1) in NAT by REAL_3:50; A11: o in RAT by A8,A9,RAT_1:def 1; reconsider o as Rational by A8,A9; set cn = c_n(r).(i+1); set cd = c_d(r).(i+1); reconsider cd as Integer by A9; o = cn/cd & cd <> 0 by A1,Th8,A8; then consider m0 such that cn = numerator(o)*m0 and A14: cd = denominator(o)*m0 by RAT_1:28; A19: cd|^2 = cd*cd by WSIERP_1:1 .= cd*(denominator(o)*m0) by A14 .= denominator(o)*denominator(o)*m0*m0 by A14 .= denominator(o)|^2*m0*m0 by WSIERP_1:1 .= denominator(o)|^2 * (m0*m0) .= denominator(o)|^2 * m0|^2 by WSIERP_1:1; A20: m0 <> 0 by A14,A1,Th8; m0 * m0 = m0^2 by SQUARE_1:def 1; then A22: m0^2 >= 0+ 1 by A20,SQUARE_1:12,INT_1:7; A23: m0|^2 = m0*m0 by WSIERP_1:1 .= m0^2 by SQUARE_1:def 1; denominator(o)|^2 <= denominator(o)|^2*m0^2 by A22,XREAL_1:151; then 1/denominator(o)|^2 >= 1/(denominator(o)|^2*m0^2) by XREAL_1:85; then |.r-o.| < 1/denominator(o)|^2 by A1,A8,A19,Th24,A23,XXREAL_0:2; hence thesis by A2,A11; end; then A28:rng f c= S; reconsider f as Function of NAT, REAL; A29:f is one-to-one proof for n1, n2 be object st n1 in dom f & n2 in dom f & f.n1 = f.n2 holds n1 = n2 proof let n1, n2 be object such that A31: n1 in dom f and A32: n2 in dom f and A33: f.n1 = f.n2; consider m1 be Nat such that A34: n1 = m1 by A31; consider m2 be Nat such that A35: n2 = m2 by A32; A36: f.m1 = f.n1 by A34 .= f.m2 by A33,A35; A37: c_n(r).(m1 +1)/c_d(r).(m1 +1) = f.m1 by A3 .= F(m2) by A36,A3 .= c_n(r).(m2 +1)/c_d(r).(m2 +1); assume n1 <> n2; then per cases by A34,A35,XXREAL_0:1; suppose m1 > m2; then m1+1 > m2+1 by XREAL_1:8; then |.r-c_n(r).(m1 +1)/c_d(r).(m1 +1).| < |.r-c_n(r).(m2 +1)/c_d(r).(m2 +1).| by A1,Th23; hence contradiction by A37; end; suppose m1 < m2; then m1+1 < m2+1 by XREAL_1:8; then |.r-c_n(r).(m1 +1)/c_d(r).(m1 +1).| > |.r-c_n(r).(m2 +1)/c_d(r).(m2 +1).| by A1,Th23; hence contradiction by A37; end; end; hence thesis; end; dom f is infinite by FUNCT_2:def 1; hence thesis by A28,A29,CARD_1:59; end; theorem r is irrational implies cocf(r) is convergent & lim (cocf(r)) = r proof assume A1: r is irrational; A2: for p be Real st 0

0; then A4: sqrt p > 0 by SQUARE_1:25; A7: [/ 1/ sqrt p \] >= 1/sqrt p by INT_1:def 7; [/ 1/ sqrt p \] > 0 by A4,INT_1:def 7; then [/ 1/ sqrt p \] in NAT by INT_1:3; then consider n such that A9: n = [/ 1/ sqrt p \]; A10: n > 0 by A4,INT_1:def 7,A9; for k be Nat st k >= n holds |. cocf(r).k-r.| < p proof let k be Nat; assume A12: k >= n; A13: cocf(r).k =( c_n(r) /" c_d(r)).k by REAL_3:def 7 .= c_n(r).k * ((c_d(r))").k by SEQ_1:8 .= c_n(r).k /c_d(r).k by VALUED_1:10; A14: |.cocf(r).k - r.| = |.-(cocf(r).k - r).| by COMPLEX1:52 .= |.r - c_n(r).k /c_d(r).k.| by A13; (1/sqrt p)^2 = (sqrt p)"*(sqrt p)" by SQUARE_1:def 1 .= (sqrt p*sqrt p)" by XCMPLX_1:204 .= (sqrt p)^2" by SQUARE_1:def 1 .= p" by A3,SQUARE_1:def 2; then n^2 >= p" by A4,A7,SQUARE_1:15,A9; then A16: (n^2)" <= (p")" by A3,XREAL_1:85; k^2 >= n^2 by A12,SQUARE_1:15; then A18: (k^2)" <= (n^2)" by A10,SQUARE_1:12,XREAL_1:85; A19: (c_d(r).k)^2 =(c_d(r).k)*(c_d(r).k) by SQUARE_1:def 1 .= c_d(r).k|^2 by WSIERP_1:1; A20: (c_d(r).k)^2 >= k^2 by A1,Th10,SQUARE_1:15; ((c_d(r).k)^2)"=(c_d(r).k|^2)" by A19 .= 1/c_d(r).k|^2; then 1/c_d(r).k|^2 <= (k^2)" by A12,A10,SQUARE_1:12,XREAL_1:85,A20; then 1/c_d(r).k|^2 <= (n^2)" by A18,XXREAL_0:2; then 1/c_d(r).k|^2 <= p by A16,XXREAL_0:2; hence thesis by XXREAL_0:2,A1,Th24,A14; end; hence thesis; end; cocf(r) is convergent by A2,SEQ_2:def 6; hence thesis by A2,SEQ_2:def 7; end; begin :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: Proof of an existence of a solution of |. x*a -y .| < 1/t x < t :: Dirichlet's argument :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: registration cluster 1_greater for Nat; existence proof take 2; thus thesis; end; end; reserve t for 1_greater Nat; Lm1: t > 0 & t > 1 & t" > 0 & t*t" = 1 proof t is 1_greater; hence thesis by XCMPLX_0:def 7; end; definition let t; func Equal_Div_interval(t) -> SetSequence of REAL means :Def1: for n be Nat holds it.n = [. n/t, n/t + t" .[; existence proof deffunc F(Element of NAT) = halfline_fin( \$1 / t, \$1 / t +t"); consider g be SetSequence of REAL such that A1: for x be Element of NAT holds g.x = F(x) from FUNCT_2:sch 4; take g; let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A1; end; uniqueness proof let i1,i2 be SetSequence of REAL; assume A2: for n be Nat holds i1.n = [. n/t, n/t + t" .[; assume A3: for n be Nat holds i2.n = [. n/t, n/t + t" .[; now let n be Element of NAT; i1.n = [. n/t, n/t + t" .[ by A2; hence i1.n=i2.n by A3; end; hence i1=i2; end; end; theorem Lm2: [.0, (k+1)/t .[ \/ [. (k+1)/t, (k+2)/t .[ = [. 0, (k+2)/t .[ proof 0 <= (k+1)/t & (k+1)/t <= (k+2)/t proof k+1 <= (k+1) + 1 by XREAL_1:31; hence thesis by XREAL_1:64; end; hence thesis by XXREAL_1:168; end; theorem Lm3: (Partial_Union Equal_Div_interval(t)).i = [.0, (i+1)/t .[ proof defpred P[Nat] means (Partial_Union Equal_Div_interval(t)).\$1 = [.0, (\$1 +1)/t .[; A1: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A2: (Partial_Union Equal_Div_interval(t)).k = [.0, (k+1)/t .[; (Partial_Union Equal_Div_interval(t)).(k+1) = (Partial_Union Equal_Div_interval(t)).k \/ (Equal_Div_interval(t)).(k+1) by PROB_3:def 2 .= [.0, (k+1)/t .[ \/ [. (k+1)/t, (k+1)/t + t" .[ by Def1,A2 .= [. 0, (k+2)/t .[ by Lm2; hence thesis; end; (Partial_Union Equal_Div_interval(t)).0 = (Equal_Div_interval(t)).0 by PROB_3:def 2 .= [. 0/t,0/t + t" .[ by Def1 .= [. 0 ,t" .[; then A3: P[0]; for n be Nat holds P[n] from NAT_1:sch 2(A3,A1); hence thesis; end; theorem Lm4: for r be Real, i be Nat st [\ r*t /] = i holds r in (Equal_Div_interval(t)).i proof let r be Real; let i be Nat; assume [\ r*t /] = i; then A3: i <= r*t & r*t -1 < i by INT_1:def 6; then i/t <= r*t/t by XREAL_1:64; then i*t" <= r*(t*t"); then A6: i*t" <= r*1 by Lm1; A7: r*t-1 + 1 < i + 1 by A3,XREAL_1:8; 0 < t" by Lm1; then (r*t)*t" < (i+1)*t" by A7,XREAL_1:68;then r*(t*t") < (i+1)*t"; then r*1 < (i+1)/t by Lm1; then r in [. i/t, i/t + t" .[ by A6,XXREAL_1:3; hence thesis by Def1; end; theorem Lm5: r1 in (Equal_Div_interval(t)).i & r2 in (Equal_Div_interval(t)).i implies |. r1 - r2 .| < t" proof assume that A2: r1 in (Equal_Div_interval(t)).i and A3: r2 in (Equal_Div_interval(t)).i; A5: r1 in [. i/t, i/t + t" .[ & r1 in [. i/t, i/t + t" .[ & r2 in [. i/t, i/t + t" .[ by A2,A3,Def1; then A6: i/t <= r1 & i/t <= r2 & r1 < i/t +t" & r2 < i/t + t" by XXREAL_1:3; per cases by XXREAL_0:1; suppose r1=r2; then |. r1 - r2 .| = 0 by ABSVALUE:2; hence thesis by Lm1; end; suppose r1 > r2; then A9: r1 - r2 > 0 by XREAL_1:50; i*t" + t" - i*t" > r1 - r2 by A6,XREAL_1:14; hence thesis by A9,ABSVALUE:def 1; end; suppose A10: r2 > r1; r2< i*t" + t" by A5,XXREAL_1:3; then A12: i*t" + t" - r1 > r2 - r1 by XREAL_1:14; i*t" <= r1 by A5,XXREAL_1:3; then A13: i*t" + t" - i*t" >= i*t" + t" - r1 by XREAL_1:13; |. r1 - r2 .| = -(r1 - r2) by A10,XREAL_1:49,ABSVALUE:def 1; hence thesis by A13,A12,XXREAL_0:2; end; end; theorem Lm6: (Partial_Union Equal_Div_interval(t)).(t-1) = [.0,1.[ proof A0: 0 <= t-1 by Lm1,XREAL_1:50; (Partial_Union Equal_Div_interval(t)).(t-1) = [. 0, (t-1 + 1)/t.[ by A0,Lm3 .= [. 0, 1 .[ by Lm1; hence thesis; end; theorem Lm7: for r be Real st r in [.0,1.[ holds ex i be Nat st i <= t-1 & r in (Equal_Div_interval(t)).i proof let r be Real; assume r in [.0,1.[; then A2: r in (Partial_Union Equal_Div_interval(t)).(t-1) by Lm6; A3: t-1 > 0 by Lm1,XREAL_1:50; t -1 in NAT by A3,INT_1:3; hence thesis by A2,PROB_3:13; end; theorem Lm8: for r be Real, i be Nat st r in (Equal_Div_interval(t)).i holds [\ r*t /] = i proof let r be Real; let i be Nat; assume A1: r in (Equal_Div_interval(t)).i; r in [. i/t, i/t + t" .[ by A1,Def1; then A3: i/t <= r & r < i/t + t" by XXREAL_1:3; then i*t"*t <= r*t by XREAL_1:64; then i*(t"*t) <= r*t;then A4: i*1 <= r*t by Lm1; t > 0 by Lm1; then r*t < (i + 1)*t" * t by A3,XREAL_1:68; then r*t < (i + 1)*(t" * t); then A6: r*t < (i + 1)*1 by Lm1; i <= r*t & r*t - 1 < i + 1 - 1 by A4,A6,XREAL_1:9; hence thesis by INT_1:def 6; end; theorem Lm9: for r be Real st r in [.0,1.[ holds ex i be Nat st i <= t-1 & [\ r*t /] = i proof let r be Real; assume r in [.0,1.[; then consider i be Nat such that A2: i <= t-1 and A3: r in (Equal_Div_interval(t)).i by Lm7; thus thesis by A2,Lm8,A3; end; definition let t,a; func F_dp1(t,a) -> FinSequence of Segm t means :Def4: len it = t+1 & for i st i in dom it holds it.i = [\ (frac ((i -1)*a))*t /]; existence proof deffunc F(Nat) = [\ (frac ((\$1 -1)*a))*t /]; consider z being FinSequence such that A1: len z = t+1 & for k being Nat st k in dom z holds z.k = F(k) from FINSEQ_1:sch 2; take z; z is FinSequence of Segm t proof A2: for y be object st y in rng z holds y in Segm t proof let y be object; assume y in rng z; then consider i be object such that A4: i in dom z and A5: y = z.i by FUNCT_1:def 3; dom z = Seg len z by FINSEQ_1:def 3 .= Seg (t+1) by A1; then consider i0 be Nat such that A7: i0 = i and 1 <= i0 and i0 <= t+ 1 by A4; reconsider i as Nat by A7; A8: z.i = F(i) by A1,A4 .= [\ (frac ((i -1)*a))*t /]; 0 <= frac ((i -1)*a) & frac ((i -1)*a) < 1 by INT_1:43; then consider j be Nat such that A10: j <= t-1 and A11: [\ (frac ((i -1)*a))*t /] = j by Lm9,XXREAL_1:3; j < t -1 + 1 by A10,XREAL_1:39; hence thesis by A5,NAT_1:44,A11,A8; end; rng z c= Segm t by A2; hence thesis by FINSEQ_1:def 4; end; hence thesis by A1; end; uniqueness proof let z1,z2 be FinSequence of Segm t such that A13:len z1 = t+1 and A14:for i be Nat st i in dom z1 holds z1.i = [\ (frac ((i-1)*a))*t /] and A15:len z2 = t+1 and A16:for i be Nat st i in dom z2 holds z2.i = [\ (frac ((i-1)*a))*t /]; A17:dom z1 = Seg len z1 by FINSEQ_1:def 3.= dom z2 by A13,A15,FINSEQ_1:def 3; for x be Nat st x in dom z1 holds z1.x = z2.x proof let x be Nat; assume A18: x in dom z1; then reconsider x9 = x as Element of NAT; thus z1.x = [\ (frac ((x9 -1)*a))*t /] by A14,A18.= z2.x by A16,A17,A18; end; hence thesis by A17; end; end; registration let t,a; cluster rng F_dp1(t,a) -> non empty; coherence proof A8: 1 < t +1 by Lm1,XREAL_1:39; dom (F_dp1(t,a)) = Seg len F_dp1(t,a) by FINSEQ_1:def 3 .= Seg (t+1) by Def4; then 1 in dom (F_dp1(t,a)) by A8; hence thesis by FUNCT_1:3; end; end; theorem Lm10: card rng(F_dp1(t,a)) in card dom(F_dp1(t,a)) proof A1: card dom (F_dp1(t,a)) = card (Seg len F_dp1(t,a)) by FINSEQ_1:def 3 .= card (Seg (t+1)) by Def4 .= t + 1 by FINSEQ_1:57; per cases; suppose A3: rng (F_dp1(t,a)) = Segm t; card Segm t in nextcard card Segm t by CARD_1:18; then card Segm t in card Segm(t+1) by NAT_1:42; hence thesis by A1,A3; end; suppose A6: rng (F_dp1(t,a)) c< Segm t; Segm t c= Segm (t+1) by NAT_1:39,XREAL_1:31; then rng (F_dp1(t,a)) c< Segm (t+1) by A6,XBOOLE_1:58; then card rng (F_dp1(t,a)) in Segm card Segm (t+1) by CARD_2:48; hence thesis by A1; end; end; Th27: ex x1, x2 st x1 in dom F_dp1(t,a) & x2 in dom F_dp1(t,a) & x1 <> x2 & F_dp1(t,a).x1 = F_dp1(t,a).x2 proof set A = dom(F_dp1(t,a)); set B = rng(F_dp1(t,a)); A1: card B in card A & B <> {} by Lm10; defpred P[object,object] means ex m1 being object st \$1 in A & \$2=m1 & (F_dp1(t,a)).\$1 = m1; A2: for x being object st x in A ex y being object st y in B & P[x,y] by FUNCT_1:3; consider h be Function of A,B such that A3: for x being object st x in A holds P[x,h.x] from FUNCT_2:sch 1(A2); consider m1,m2 be object such that A4: m1 in A and A5: m2 in A and A6: m1 <> m2 and A7: h.m1 = h.m2 by A1,FINSEQ_4:65; A9: P[m2,h.m2] by A3,A5; P[m1,h.m1] by A3,A4; then (F_dp1(t,a)).m1 = h.m2 by A7 .= (F_dp1(t,a)).m2 by A9; hence thesis by A4,A5,A6; end; registration let t,a; cluster F_dp1 (t,a) -> non one-to-one; coherence proof assume a1: F_dp1 (t,a) is one-to-one; consider x1, x2 such that A2: x1 in dom (F_dp1(t,a)) & x2 in dom (F_dp1(t,a)) & x1 <> x2 & F_dp1(t,a).x1 = F_dp1(t,a).x2 by Th27; thus thesis by a1,A2; end; end; begin :: Proof of Dirichlet's Theorem ::[Baker] Chapter 6.1 ::\$N Dirichlet's approximation theorem theorem ex x,y be Integer st |. x*a - y .| < 1/t & 0 < x & x <= t proof consider x1, x2 be object such that A1: x1 in dom (F_dp1(t,a)) and A2: x2 in dom (F_dp1(t,a)) and A3: x1 <> x2 and A4: F_dp1(t,a).x1 = F_dp1(t,a).x2 by Th27; A5: dom (F_dp1(t,a)) = Seg len F_dp1(t,a) by FINSEQ_1:def 3 .= Seg (t+1) by Def4; consider n1 be Nat such that A6: x1 = n1 and A7: 1<= n1 and A8: n1 <= t+1 by A1, A5; reconsider x1 as Nat by A6; consider n2 be Nat such that A9: x2 = n2 and A10: 1 <= n2 and A11: n2 <= t+1 by A2,A5; reconsider x2 as Nat by A9; F_dp1(t,a).x1 in rng F_dp1(t,a) by A1,FUNCT_1:3;then F_dp1(t,a).x1 in Segm t; then F_dp1(t,a).x1 in { i where i is Nat : i < t } by AXIOMS:4; then consider i be Nat such that A13: F_dp1(t,a).x1 = i and i < t; A14: [\ (frac ((x1 -1)*a))*t /] = i by Def4,A1,A13; reconsider r1 = frac ((x1 -1)*a) as Real; F_dp1(t,a).x2 in rng F_dp1(t,a) by A2,FUNCT_1:3;then F_dp1(t,a).x2 in Segm t; then F_dp1(t,a).x2 in { i where i is Nat : i < t } by AXIOMS:4; then consider i2 be Nat such that A16: F_dp1(t,a).x2 = i2 and i2 < t; A17: [\ (frac ((x2 -1)*a))*t /] = i2 by Def4,A2,A16; reconsider r2 = frac ((x2 -1)*a) as Real; i = F_dp1(t,a).x1 by A13 .= F_dp1(t,a).x2 by A4 .= i2 by A16; then A18: r1 in (Equal_Div_interval(t)).i & r2 in (Equal_Div_interval(t)).i by A14,Lm4,A17; A19: |. r1 - r2 .| < t" by Lm5,A18; set m1 = x1 - 1; set m2 = x2 - 1; A20: r1 - r2 = m1*a - [\ m1*a /] - frac (m2*a) by INT_1:def 8 .= m1*a - [\ m1*a /] - (m2*a - [\ m2*a /]) by INT_1:def 8 .= (m1-m2)*a -( [\ m1*a /] - [\ m2*a /]); per cases by A3,XXREAL_0:1; suppose A21: x1 > x2; set x = m1 - m2; set y = [\ m1*a /] - [\ m2*a /]; A24: x = x1 - x2; A25: t+1 - x2 >= x1 - x2 by A6,A8,XREAL_1:13; t+1 - 1 >= t + 1 - x2 by A9,A10,XREAL_1:10; then A27: x <= t by A25,XXREAL_0:2; A28: 0 < x by A21,XREAL_1:50,A24; |. x*a -y .| < t" by Lm5,A18,A20; hence thesis by A27,A28; end; suppose A29: x1 < x2; set x = m2 - m1; set y = [\ m2*a /] - [\ m1*a /]; A32: x = x2 - x1; A33: t+1 - x1 >= x2 - x1 by A9,A11,XREAL_1:13; t+1 - 1 >= t + 1 - x1 by A6,A7,XREAL_1:10; then A35: x <= t by A33,XXREAL_0:2; A36: 0 < x by A29,XREAL_1:50,A32; -(r1-r2) = x*a - y by A20; then |. x*a -y .| < t" by A19,COMPLEX1:52; hence thesis by A35,A36; end; end;