assume HWZSet1 r is finite ; :: thesis: contradiction
then reconsider HWS1 = HWZSet1 r as non empty finite Subset of NAT ;
reconsider j = max HWS1 as Element of NAT by ORDINAL1:def 12;
HWS1 c= REAL by NUMBERS:19;
then reconsider HWS1 = HWS1 as non empty Subset of ExtREAL by NUMBERS:31, XBOOLE_1:1;
A4: for s being Element of HWS1 holds
( j >= s & j > 0 )
proof
let s be Element of HWS1; :: thesis: ( j >= s & j > 0 )
A5: s in HWS1 by SUBSET_1:def 1;
then j >= s by XXREAL_2:4;
hence ( j >= s & j > 0 ) by A5, Th10; :: thesis: verum
end;
set n = j + 1;
per cases ( |.(r - (((c_n r) . (j + 1)) / ((c_d r) . (j + 1)))).| < 1 / ((sqrt 5) * (((c_d r) . (j + 1)) |^ 2)) or |.(r - (((c_n r) . ((j + 1) + 1)) / ((c_d r) . ((j + 1) + 1)))).| < 1 / ((sqrt 5) * (((c_d r) . ((j + 1) + 1)) |^ 2)) or |.(r - (((c_n r) . ((j + 1) + 2)) / ((c_d r) . ((j + 1) + 2)))).| < 1 / ((sqrt 5) * (((c_d r) . ((j + 1) + 2)) |^ 2)) ) by Th5, A4, XREAL_1:29;
suppose A7: |.(r - (((c_n r) . (j + 1)) / ((c_d r) . (j + 1)))).| < 1 / ((sqrt 5) * (((c_d r) . (j + 1)) |^ 2)) ; :: thesis: contradiction
set q1 = (c_n r) . (j + 1);
set q2 = (c_d r) . (j + 1);
set q = ((c_n r) . (j + 1)) / ((c_d r) . (j + 1));
A9: (c_n r) . (j + 1),(c_d r) . (j + 1) are_coprime by Th4;
( (c_n r) . (j + 1) = numerator (((c_n r) . (j + 1)) / ((c_d r) . (j + 1))) & (c_d r) . (j + 1) = denominator (((c_n r) . (j + 1)) / ((c_d r) . (j + 1))) ) by Th8, A9;
then ((c_n r) . (j + 1)) / ((c_d r) . (j + 1)) in HWZSet r by A7;
then denominator (((c_n r) . (j + 1)) / ((c_d r) . (j + 1))) in HWZSet1 r ;
then A14: (c_d r) . (j + 1) in HWZSet1 r by Th8, A9;
A15: (c_d r) . (j + 1) >= j + 1 by DIOPHAN1:9;
j + 1 > j by XREAL_1:29;
then (c_d r) . (j + 1) > j by A15, XXREAL_0:2;
hence contradiction by A4, A14; :: thesis: verum
end;
suppose A17: |.(r - (((c_n r) . ((j + 1) + 1)) / ((c_d r) . ((j + 1) + 1)))).| < 1 / ((sqrt 5) * (((c_d r) . ((j + 1) + 1)) |^ 2)) ; :: thesis: contradiction
set q1 = (c_n r) . ((j + 1) + 1);
set q2 = (c_d r) . ((j + 1) + 1);
set q = ((c_n r) . ((j + 1) + 1)) / ((c_d r) . ((j + 1) + 1));
A19: (c_n r) . ((j + 1) + 1),(c_d r) . ((j + 1) + 1) are_coprime by Th4;
then A20: ( (c_n r) . ((j + 1) + 1) = numerator (((c_n r) . ((j + 1) + 1)) / ((c_d r) . ((j + 1) + 1))) & (c_d r) . ((j + 1) + 1) = denominator (((c_n r) . ((j + 1) + 1)) / ((c_d r) . ((j + 1) + 1))) ) by Th8;
|.(r - (((c_n r) . ((j + 1) + 1)) / ((c_d r) . ((j + 1) + 1)))).| < 1 / ((sqrt 5) * ((denominator (((c_n r) . ((j + 1) + 1)) / ((c_d r) . ((j + 1) + 1)))) |^ 2)) by A17, Th8, A19;
then ((c_n r) . ((j + 1) + 1)) / ((c_d r) . ((j + 1) + 1)) in HWZSet r ;
then (c_d r) . ((j + 1) + 1) in HWZSet1 r by A20;
then A23: (c_d r) . ((j + 1) + 1) <= j by A4;
A24: (c_d r) . ((j + 1) + 1) >= j + 2 by DIOPHAN1:9;
j + 2 > j by XREAL_1:29;
hence contradiction by A23, A24, XXREAL_0:2; :: thesis: verum
end;
suppose A26: |.(r - (((c_n r) . ((j + 1) + 2)) / ((c_d r) . ((j + 1) + 2)))).| < 1 / ((sqrt 5) * (((c_d r) . ((j + 1) + 2)) |^ 2)) ; :: thesis: contradiction
set q1 = (c_n r) . ((j + 1) + 2);
set q2 = (c_d r) . ((j + 1) + 2);
set q = ((c_n r) . ((j + 1) + 2)) / ((c_d r) . ((j + 1) + 2));
A28: (c_n r) . ((j + 1) + 2),(c_d r) . ((j + 1) + 2) are_coprime by Th4;
then A29: ( (c_n r) . ((j + 1) + 2) = numerator (((c_n r) . ((j + 1) + 2)) / ((c_d r) . ((j + 1) + 2))) & (c_d r) . ((j + 1) + 2) = denominator (((c_n r) . ((j + 1) + 2)) / ((c_d r) . ((j + 1) + 2))) ) by Th8;
|.(r - (((c_n r) . ((j + 1) + 2)) / ((c_d r) . ((j + 1) + 2)))).| < 1 / ((sqrt 5) * ((denominator (((c_n r) . ((j + 1) + 2)) / ((c_d r) . ((j + 1) + 2)))) |^ 2)) by Th8, A28, A26;
then ((c_n r) . ((j + 1) + 2)) / ((c_d r) . ((j + 1) + 2)) in HWZSet r ;
then (c_d r) . ((j + 1) + 2) in HWZSet1 r by A29;
then A33: (c_d r) . ((j + 1) + 2) <= j by A4;
A34: (c_d r) . ((j + 1) + 2) >= j + 3 by DIOPHAN1:9;
j + 3 > j by XREAL_1:29;
hence contradiction by A33, A34, XXREAL_0:2; :: thesis: verum
end;
end;