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;