let a, b be Integer; :: thesis: ( ( a divides b implies a divides - b ) & ( a divides - b implies a divides b ) & ( a divides b implies - a divides b ) & ( - a divides b implies a divides b ) & ( a divides b implies - a divides - b ) & ( - a divides - b implies a divides b ) & ( a divides - b implies - a divides b ) & ( - a divides b implies a divides - b ) )
A1: ( a divides b implies a divides - b )

proof

assume A2: a divides b ; :: thesis: a divides - b
b divides - b by Lm1;
hence a divides - b by A2, Lm2; :: thesis: verum

end;

A3: ( a divides - b implies a divides b )

proof

assume A4: a divides - b ; :: thesis: a divides b
- b divides b by Lm1;
hence a divides b by A4, Lm2; :: thesis: verum

end;

hence ( a divides b iff a divides - b ) by A1; :: thesis: ( ( a divides b implies - a divides b ) & ( - a divides b implies a divides b ) & ( a divides b implies - a divides - b ) & ( - a divides - b implies a divides b ) & ( a divides - b implies - a divides b ) & ( - a divides b implies a divides - b ) )
A5: ( - a divides b implies a divides b )

proof

assume A6: - a divides b ; :: thesis: a divides b
a divides - a by Lm1;
hence a divides b by A6, Lm2; :: thesis: verum

end;

A7: ( - a divides - b implies a divides b )

proof

assume A8: - a divides - b ; :: thesis: a divides b
- b divides b by Lm1;
hence a divides b by A5, A8, Lm2; :: thesis: verum

end;

A9: ( a divides b implies - a divides b )

proof

assume A10: a divides b ; :: thesis: - a divides b
- a divides a by Lm1;
hence - a divides b by A10, Lm2; :: thesis: verum

end;

hence ( a divides b iff - a divides b ) by A5; :: thesis: ( ( a divides b implies - a divides - b ) & ( - a divides - b implies a divides b ) & ( a divides - b implies - a divides b ) & ( - a divides b implies a divides - b ) )
( a divides b implies - a divides - b )

proof

assume A11: a divides b ; :: thesis: - a divides - b
- a divides a by Lm1;
hence - a divides - b by A1, A11, Lm2; :: thesis: verum

end;

hence ( a divides b iff - a divides - b ) by A7; :: thesis: ( a divides - b iff - a divides b )
thus ( a divides - b iff - a divides b ) by A1, A3, A9, A5; :: thesis: verum