let a, b be Integer; :: thesis: ( a divides b & b divides a & not a = b implies a = - b )
assume that
A1: a divides b and
A2: b divides a ; :: thesis: ( a = b or a = - b )
consider a1 being Integer such that
A3: b = a * a1 by A1;
consider b1 being Integer such that
A4: a = b * b1 by A2;
( not a <> 0 or a = b or a = - b )
proof
assume A5: a <> 0 ; :: thesis: ( a = b or a = - b )
1 * a = a * (a1 * b1) by A3, A4;
then a1 * b1 = 1 by A5, XCMPLX_1:5;
then ( a = b * 1 or a = b * (- 1) ) by A4, INT_1:9;
hence ( a = b or a = - b ) ; :: thesis: verum
end;
hence ( a = b or a = - b ) by A1; :: thesis: verum