PROOF 07
Prove.
a − b = a + (−b)
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 − b denotes the x satisfying x + b = a.
Proof.
Subtraction asks addition in reverse. This definition does not yet say whether such an x exists.convention
∎
Lemma L1
For all a, b, (a + (−b)) + b = a
Proof.
(1)(a + (−b)) + b = a + ((−b) + b)A2
(2)(−b) + b = b + (−b)A4
(3) = 0A3
(4)(a + (−b)) + b = a + 0(1), (3), E
(5) = aA1
∎
Lemma L2
If x + b = a and y + b = a, then x = y
Proof.
(1)x = x + 0A1
(2) = x + (b + (−b))A3
(3) = (x + b) + (−b)A2
(4) = a + (−b)assumption
(5)By the same computation, y = a + (−b)A1, A3, A2, assumption
(6)x = y(4), (5)
∎
Theorem T
a − b = a + (−b)
Proof.
(1)a + (−b) satisfies x + b = a.L1
(2)At most one x satisfies it.L2
(3)Therefore the value D1 determines is a + (−b), and only that.D1, (1), (2)
∎
Remark
Can A3 be removed from this proof?
Check the lines where −b appears, one by one.