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 ) )
thus A1: ( a divides b iff a divides - b ) :: 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 ) )

proof

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

proof

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

end;

( 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 A2; :: thesis: verum

end;

thus A5: ( a divides b iff - a divides b ) :: 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 ) )

proof

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

proof

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

end;

( - a divides b implies a divides b )

proof

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

end;

hence ( a divides b iff - a divides b ) by A6; :: thesis: verum

end;

thus ( a divides b iff - a divides - b ) :: thesis: ( a divides - b iff - a divides b )

proof

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 A1, A10, Lm2; :: thesis: verum

end;

( - a divides - b implies a divides b )

proof

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

end;

hence ( a divides b iff - a divides - b ) by A9; :: thesis: verum

end;

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