let n be Nat; :: thesis: for r being Real st r is irrational & n > 0 holds
|.(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)))).|
let r be Real; :: thesis: ( 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)))).| )
assume that
A1: r is irrational and
A2: n > 0 ; :: thesis: |.(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)))).|

per cases ( n is even or n is odd ) ;

suppose A3: n is even ; :: thesis: |.(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)))).|

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 |.(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)))).| by A10, ABSVALUE:def 1; :: thesis: verum

end;

suppose A11: n is odd ; :: thesis: |.(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)))).|

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 |.(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)))).| by A14, A19, ABSVALUE:def 1; :: thesis: verum

end;

end;