let n be Integer; :: thesis: ( n <> 0 & n <> - 1 & n <> - 2 implies not n / (n + 1) in INT )
assume AS: ( n <> 0 & n <> - 1 & n <> - 2 ) ; :: thesis: not n / (n + 1) in INT
consider m being Nat such that
A0: ( n = m or n = - m ) by INT_1:2;

per cases ( n = m or n = - m ) by A0;

suppose n = m ; :: thesis: not n / (n + 1) in INT

hence not n / (n + 1) in INT by AS, NAT_1:16, NAT_D:33; :: thesis: verum

end;

suppose D1: n = - m ; :: thesis: not n / (n + 1) in INT

then D2: n / (n + 1) = (- m) / (- (m - 1))
.= m / (m - 1) by XCMPLX_1:191
.= ((m - 1) / (m - 1)) + (1 / (m - 1)) ;
D32: ( m <> 0 & m <> 1 & m <> 2 ) by D1, AS;
then 1 <= m by NAT_1:14;
then 1 < m by AS, D1, XXREAL_0:1;
then 1 + 1 <= m by NAT_1:13;
then 2 < m by AS, D1, XXREAL_0:1;
then 2 + 1 <= m by NAT_1:13;
then D3: (2 + 1) - 1 <= m - 1 by XREAL_1:9;
then D31: ( 1 < m - 1 & m - 1 <> 0 ) by XXREAL_0:2;
D4: n / (n + 1) = 1 + (1 / (m - 1)) by D2, D3, XCMPLX_1:60;
thus not n / (n + 1) in INT :: thesis: verum

proof

assume n / (n + 1) in INT ; :: thesis: contradiction
then reconsider k = n / (n + 1) as Integer ;
D5: k - 1 = 1 / (m - 1) by D4;
reconsider j = m - 1 as Nat by D32;
1 / j is not Integer by D31, NAT_D:33;
hence contradiction by D5; :: thesis: verum

end;

end;

end;