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