let a be Real; for t being 1 _greater Nat ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t )
let t be 1 _greater Nat; ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t )
consider x1, x2 being 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 being Nat such that
A6:
x1 = n1
and
A7:
1 <= n1
and
A8:
n1 <= t + 1
by A1, A5;
reconsider x1 = x1 as Nat by A6;
consider n2 being Nat such that
A9:
x2 = n2
and
A10:
1 <= n2
and
A11:
n2 <= t + 1
by A2, A5;
reconsider x2 = 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 being 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 being 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 =
(((x1 - 1) * a) - [\((x1 - 1) * a)/]) - (frac ((x2 - 1) * a))
by INT_1:def 8
.=
(((x1 - 1) * a) - [\((x1 - 1) * a)/]) - (((x2 - 1) * a) - [\((x2 - 1) * a)/])
by INT_1:def 8
.=
(((x1 - 1) - (x2 - 1)) * a) - ([\((x1 - 1) * a)/] - [\((x2 - 1) * a)/])
;
per cases
( x1 > x2 or x1 < x2 )
by A3, XXREAL_0:1;
suppose A21:
x1 > x2
;
ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t )set x =
(x1 - 1) - (x2 - 1);
set y =
[\((x1 - 1) * a)/] - [\((x2 - 1) * a)/];
A24:
(x1 - 1) - (x2 - 1) = 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:
(x1 - 1) - (x2 - 1) <= t
by A25, XXREAL_0:2;
A28:
0 < (x1 - 1) - (x2 - 1)
by A21, XREAL_1:50, A24;
|.((((x1 - 1) - (x2 - 1)) * a) - ([\((x1 - 1) * a)/] - [\((x2 - 1) * a)/])).| < t "
by Lm5, A18, A20;
hence
ex
x,
y being
Integer st
(
|.((x * a) - y).| < 1
/ t &
0 < x &
x <= t )
by A27, A28;
verum end; suppose A29:
x1 < x2
;
ex x, y being Integer st
( |.((x * a) - y).| < 1 / t & 0 < x & x <= t )set x =
(x2 - 1) - (x1 - 1);
set y =
[\((x2 - 1) * a)/] - [\((x1 - 1) * a)/];
A32:
(x2 - 1) - (x1 - 1) = 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:
(x2 - 1) - (x1 - 1) <= t
by A33, XXREAL_0:2;
A36:
0 < (x2 - 1) - (x1 - 1)
by A29, XREAL_1:50, A32;
- (r1 - r2) = (((x2 - 1) - (x1 - 1)) * a) - ([\((x2 - 1) * a)/] - [\((x1 - 1) * a)/])
by A20;
then
|.((((x2 - 1) - (x1 - 1)) * a) - ([\((x2 - 1) * a)/] - [\((x1 - 1) * a)/])).| < t "
by A19, COMPLEX1:52;
hence
ex
x,
y being
Integer st
(
|.((x * a) - y).| < 1
/ t &
0 < x &
x <= t )
by A35, A36;
verum end;