let i be Integer; :: thesis: ( (- 3) / 2 < i & i < 1 / 2 & not i = 0 implies i = - 1 )
assume A1: ( (- 3) / 2 < i & i < 1 / 2 ) ; :: thesis: ( i = 0 or i = - 1 )
assume A2: ( not i = 0 & not i = - 1 ) ; :: thesis: contradiction
( - 2 < i & i < 1 ) by A1, XXREAL_0:2;
then A3: ( (- 2) + 1 <= i & i + 1 <= 1 & 0 <= 1 ) by INT_1:7;
then A4: ( - 1 <= i & (i + 1) - 1 <= 1 - 1 ) by XREAL_1:9;
consider k being Nat such that
A5: ( i = k or i = - k ) by INT_1:2;
per cases ( i = k or i = - k ) by A5;
suppose i = k ; :: thesis: contradiction
hence contradiction by A2, A4; :: thesis: verum
end;
suppose A6: i = - k ; :: thesis: contradiction
then (- k) * (- 1) <= (- 1) * (- 1) by A3, XREAL_1:65;
then not not k = 0 & ... & not k = 1 ;
hence contradiction by A6, A2; :: thesis: verum
end;
end;