PROOF 81
Prove.
(−a)b = −(ab)
On the integers ℤ.
A way to read this proof
First separate what is assumed from what is to be proved. At each step, ask which definition or earlier result permits the move. If it is unclear, return to that premise rather than skipping to the conclusion.
Definition D1
−a denotes the x satisfying a + x = 0.
Proof.
The existence of such an x is guaranteed by A4; its uniqueness by A5.A4, A5
∎
Lemma L1
For every a, a × 0 = 0
Proof.
(1)0 + 0 = 0A1
(2)a(0 + 0) = a × 0(1), E
(3)a×0 + a×0 = a×0(2), A6
(4)(a×0 + a×0) + (−(a×0)) = a×0 + (−(a×0))(3), E
(5)a×0 + (a×0 + (−(a×0))) = 0(4), A2, A4
(6)a×0 + 0 = 0(5), A4
(7)a × 0 = 0(6), A1
∎
Theorem T
For all a, b, (−a)b = −(ab)
Proof.
(1)(−a) + a = 0D1, A3
(2)((−a) + a)b = 0 × b(1), E
(3)((−a) + a)b = b((−a) + a) = b(−a) + baA7, A6
(4) = (−a)b + ab(3), A7
(5)0 × b = b × 0 = 0A7, L1
(6)(−a)b + ab = 0(2), (4), (5)
(7)(−(ab)) + ab = 0D1, A3
(8)Both are additive inverses of ab, hence (−a)b = −(ab)(6), (7), A5
∎
Corollary C
For all a, b, (−a)(−b) = ab
Proof.
(1)(−a)(−b) = −(a(−b))T
(2)a(−b) = (−b)a = −(ba) = −(ab)A7, T
(3)(−a)(−b) = −(−(ab))(1), (2), E
(4)ab + (−(ab)) = 0 and (−(−(ab))) + (−(ab)) = 0D1, A3
(5)−(−(ab)) = ab(4), A5
(6)Therefore (−a)(−b) = ab(3), (5)
∎
Remark
Can A6 be removed from this proof?
(−a)b is never computed anywhere. Find the line where its value is actually pinned down.