let r be Real; :: thesis: ( [\r/] = [/r\] iff not [\r/] + 1 = [/r\] )
set Diff = [/r\] + (- [\r/]);
A1: now :: thesis: ( r is not Integer implies ( [\r/] + 1 = [/r\] & [\r/] <> [/r\] ) )
assume r is not Integer ; :: thesis: ( [\r/] + 1 = [/r\] & [\r/] <> [/r\] )
then [\r/] < [/r\] by Th35;
then [\r/] + (- [\r/]) < [/r\] + (- [\r/]) by XREAL_1:6;
then A2: 1 <= [/r\] + (- [\r/]) by Lm4;
r - 1 < [\r/] by Def6;
then A3: - [\r/] < - (r - 1) by XREAL_1:24;
[/r\] < r + 1 by Def7;
then [/r\] + (- [\r/]) < (r + 1) + (- (r - 1)) by A3, XREAL_1:8;
then (([/r\] + (- [\r/])) + 1) + (- 1) <= (1 + 1) + (- 1) by Th7;
then [\r/] + 1 = [\r/] + ([/r\] + (- [\r/])) by A2, XXREAL_0:1;
hence ( [\r/] + 1 = [/r\] & [\r/] <> [/r\] ) ; :: thesis: verum
end;
now :: thesis: ( r is Integer implies ( [\r/] = [/r\] & [\r/] + 1 <> [/r\] ) )
assume r is Integer ; :: thesis: ( [\r/] = [/r\] & [\r/] + 1 <> [/r\] )
then [\r/] = [/r\] by Th34;
hence ( [\r/] = [/r\] & [\r/] + 1 <> [/r\] ) ; :: thesis: verum
end;
hence ( [\r/] = [/r\] iff not [\r/] + 1 = [/r\] ) by A1; :: thesis: verum