let a, b be Integer; :: thesis: ( |.a.| <> |.b.| implies ( a - b <> 0 & a + b <> 0 ) )
assume A0: |.a.| <> |.b.| ; :: thesis: ( a - b <> 0 & a + b <> 0 )

per cases ( |.a.| = a or |.a.| = - a ) by ABSVALUE:1;

suppose A1: |.a.| = a ; :: thesis: ( a - b <> 0 & a + b <> 0 )

per cases ( |.b.| = b or |.b.| = - b ) by ABSVALUE:1;

suppose A2: |.b.| = b ; :: thesis: ( a - b <> 0 & a + b <> 0 )

( a <> b & ( a <> 0 or b <> 0 ) ) by A0;
hence ( a - b <> 0 & a + b <> 0 ) by A1, A2; :: thesis: verum

end;

suppose |.b.| = - b ; :: thesis: ( a - b <> 0 & a + b <> 0 )

hence ( a - b <> 0 & a + b <> 0 ) by A0; :: thesis: verum

end;

end;

end;

suppose |.a.| = - a ; :: thesis: ( a - b <> 0 & a + b <> 0 )

hence ( a - b <> 0 & a + b <> 0 ) by A0; :: thesis: verum

end;

end;