let n, m, i, j be Nat; :: thesis: ( |.(i - j).| + |.(n - m).| = 1 iff ( ( |.(i - j).| = 1 & n = m ) or ( |.(n - m).| = 1 & i = j ) ) )
thus ( not |.(i - j).| + |.(n - m).| = 1 or ( |.(i - j).| = 1 & n = m ) or ( |.(n - m).| = 1 & i = j ) ) :: thesis: ( ( ( |.(i - j).| = 1 & n = m ) or ( |.(n - m).| = 1 & i = j ) ) implies |.(i - j).| + |.(n - m).| = 1 )

proof

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

now :: thesis: ( ( |.(i - j).| = 1 & n = m ) or ( |.(n - m).| = 1 & i = j ) )

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

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

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

end;

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

now :: thesis: ( ( |.(i - j).| = 1 & n = m ) or ( |.(n - m).| = 1 & i = j ) )

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

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

reconsider l = m - n as Element of NAT by INT_1:5, A4;
0 < l by A4, XREAL_1:50;
then A5: 0 + 1 <= l by NAT_1:13;
A6: |.(- (m - n)).| = |.l.| by COMPLEX1:52;
then A7: |.(n - m).| = |.l.| ;
A8: |.l.| = l by ABSVALUE:def 1;
then A9: l <= 1 by A1, A6, COMPLEX1:46, XREAL_1:31;
then l = 1 by A5, XXREAL_0:1;
then i - j = 0 by A1, A8, A7, ABSVALUE:2;
hence ( ( |.(i - j).| = 1 & n = m ) or ( |.(n - m).| = 1 & i = j ) ) by A6, A5, A8, A9, XXREAL_0:1; :: thesis: verum

end;

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

then reconsider l = n - m as Element of NAT by INT_1:5;
0 < l by A10, XREAL_1:50;
then A11: 0 + 1 <= l by NAT_1:13;
A12: |.(n - m).| = l by ABSVALUE:def 1;
then A13: l <= 1 by A1, COMPLEX1:46, XREAL_1:31;
then l = 1 by A11, XXREAL_0:1;
then i - j = 0 by A1, A12, ABSVALUE:2;
hence ( ( |.(i - j).| = 1 & n = m ) or ( |.(n - m).| = 1 & i = j ) ) by A11, A12, A13, XXREAL_0:1; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

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

now :: thesis: |.(i - j).| + |.(n - m).| = 1

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

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

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

end;

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

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

end;

end;

end;

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