let S be Subset of RAT; :: thesis: for r being Real st r is irrational & S = { p where p is Element of RAT : |.(r - p).| < 1 / ((denominator p) |^ 2) } holds
S is infinite
let r be Real; :: thesis: ( r is irrational & S = { p where p is Element of RAT : |.(r - p).| < 1 / ((denominator p) |^ 2) } implies S is infinite )
assume that
A1: r is irrational and
A2: S = { p where p is Element of RAT : |.(r - p).| < 1 / ((denominator p) |^ 2) } ; :: thesis: S is infinite
deffunc H₁( Nat) -> Element of REAL = ((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 = H₁(n) from SEQ_1:sch 1();
for o being Real st o in rng f holds
o in S

proof

let o be Real; :: thesis: ( o in rng f implies o in S )
assume o in rng f ; :: thesis: o in S
then consider i being object such that
A6: i in dom f and
A7: o = f . i by FUNCT_1:def 3;
reconsider i = i as Nat by A6;
A8: o = H₁(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 = o as Rational by A8, A9;
set cn = (c_n r) . (i + 1);
set cd = (c_d r) . (i + 1);
reconsider cd = (c_d r) . (i + 1) as Integer by A9;
( o = ((c_n r) . (i + 1)) / cd & cd <> 0 ) by A1, Th8, A8;
then consider m0 being Integer such that
(c_n r) . (i + 1) = (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 o in S by A2, A11; :: thesis: verum

end;

then A28: rng f c= S ;
reconsider f = f as Function of NAT,REAL ;
A29: f is one-to-one

proof

for n1, n2 being object st n1 in dom f & n2 in dom f & f . n1 = f . n2 holds
n1 = n2

proof

let n1, n2 be object ; :: thesis: ( n1 in dom f & n2 in dom f & f . n1 = f . n2 implies n1 = n2 )
assume that
A31: n1 in dom f and
A32: n2 in dom f and
A33: f . n1 = f . n2 ; :: thesis: n1 = n2
consider m1 being Nat such that
A34: n1 = m1 by A31;
consider m2 being 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
.= H₁(m2) by A36, A3
.= ((c_n r) . (m2 + 1)) / ((c_d r) . (m2 + 1)) ;
assume n1 <> n2 ; :: thesis: contradiction

per cases then ( m1 > m2 or m1 < m2 ) by A34, A35, XXREAL_0:1;

suppose m1 > m2 ; :: thesis: contradiction

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; :: thesis: verum

end;

suppose m1 < m2 ; :: thesis: contradiction

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; :: thesis: verum

end;

end;

end;

hence f is one-to-one ; :: thesis: verum

end;

dom f is infinite by FUNCT_2:def 1;
hence S is infinite by A28, A29, CARD_1:59; :: thesis: verum