let i, j, n, m be Element of NAT ; :: thesis: ( (abs (i - j)) + (abs (n - m)) = 1 iff ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) )
thus ( not (abs (i - j)) + (abs (n - m)) = 1 or ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) :: thesis: ( ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) implies (abs (i - j)) + (abs (n - m)) = 1 )

proof

assume A1: (abs (i - j)) + (abs (n - m)) = 1 ; :: thesis: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) )

now

per cases ( n = m or n <> m ) ;

suppose A2: n = m ; :: thesis: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) )

then 1 = (abs (i - j)) + 0 by A1, ABSVALUE:7
.= abs (i - j) ;
hence ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) by A2; :: thesis: verum

end;

suppose A3: n <> m ; :: thesis: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) )

now

per cases ( n < m or n > m ) by A3, XXREAL_0:1;

suppose A4: n < m ; :: thesis: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) )

then reconsider l = m - n as Element of NAT by INT_1:18;
0 < l by A4, XREAL_1:52;
then A5: 0 + 1 <= l by NAT_1:13;
A6: abs (- (m - n)) = abs l by COMPLEX1:138;
then A7: abs (n - m) = abs l ;
A8: abs l = l by ABSVALUE:def 1;
then A9: l <= 1 by A1, A6, COMPLEX1:132, XREAL_1:33;
then l = 1 by A5, XXREAL_0:1;
then i - j = 0 by A1, A8, A7, ABSVALUE:7;
hence ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) by A6, A5, A8, A9, XXREAL_0:1; :: thesis: verum

end;

suppose A10: n > m ; :: thesis: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) )

then reconsider l = n - m as Element of NAT by INT_1:18;
0 < l by A10, XREAL_1:52;
then A11: 0 + 1 <= l by NAT_1:13;
A12: abs (n - m) = l by ABSVALUE:def 1;
then A13: l <= 1 by A1, COMPLEX1:132, XREAL_1:33;
then l = 1 by A11, XXREAL_0:1;
then i - j = 0 by A1, A12, ABSVALUE:7;
hence ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) by A11, A12, A13, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) ; :: thesis: verum

end;

end;

end;

hence ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) ; :: thesis: verum

end;

assume A14: ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) ; :: thesis: (abs (i - j)) + (abs (n - m)) = 1

now

per cases ( ( abs (i - j) = 1 & n = m ) or ( abs (n - m) = 1 & i = j ) ) by A14;

suppose A15: ( abs (i - j) = 1 & n = m ) ; :: thesis: (abs (i - j)) + (abs (n - m)) = 1

then abs (n - m) = 0 by ABSVALUE:7;
hence (abs (i - j)) + (abs (n - m)) = 1 by A15; :: thesis: verum

end;

suppose A16: ( abs (n - m) = 1 & i = j ) ; :: thesis: (abs (i - j)) + (abs (n - m)) = 1

then abs (i - j) = 0 by ABSVALUE:7;
hence (abs (i - j)) + (abs (n - m)) = 1 by A16; :: thesis: verum

end;

end;

end;

hence (abs (i - j)) + (abs (n - m)) = 1 ; :: thesis: verum