let r, s be Real; :: thesis: ( |.(r - s).| = 1 iff ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) )
thus ( not |.(r - s).| = 1 or ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) :: thesis: ( ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) implies |.(r - s).| = 1 )
proof
assume A1: |.(r - s).| = 1 ; :: thesis: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) )
now :: thesis: ( ( r > s & ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) ) or ( r = s & contradiction ) or ( r < s & ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) ) )
per cases ( r > s or r = s or r < s ) by XXREAL_0:1;
case A2: r > s ; :: thesis: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) )
then 0 < r - s by XREAL_1:50;
then r - s = 1 by A1, ABSVALUE:def 1;
hence ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) by A2; :: thesis: verum
end;
case A3: r < s ; :: thesis: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) )
then A4: 0 < s - r by XREAL_1:50;
1 = |.(- (r - s)).| by A1, COMPLEX1:52
.= s - r by A4, ABSVALUE:def 1 ;
hence ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) by A3; :: thesis: verum
end;
end;
end;
hence ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) ; :: thesis: verum
end;
assume A5: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) ; :: thesis: |.(r - s).| = 1
per cases ( ( r > s & r = s + 1 ) or ( s > r & s = r + 1 ) ) by A5;
suppose ( r > s & r = s + 1 ) ; :: thesis: |.(r - s).| = 1
hence |.(r - s).| = 1 by ABSVALUE:def 1; :: thesis: verum
end;
suppose A6: ( s > r & s = r + 1 ) ; :: thesis: |.(r - s).| = 1
thus |.(r - s).| = |.(- (r - s)).| by COMPLEX1:52
.= 1 by A6, ABSVALUE:def 1 ; :: thesis: verum
end;
end;