PROOF 79
Prove.
a × 0 = 0
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.
Theorem T1
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), A4
(4)(a×0 + a×0) + (−(a×0)) = a×0 + (−(a×0))(3), E
(5)a×0 + (a×0 + (−(a×0))) = a×0 + (−(a×0))(4), A2
(6)a×0 + 0 = 0(5), A3
(7)a × 0 = 0(6), A1
∎
Corollary C
For every a, 0 × a = 0
Proof.
(1)0 × a = a × 0A5
(2)a × 0 = 0T1
(3)0 × a = 0(1), (2)
∎
Remark
Can A4 be removed from this proof?
In this list only one axiom links multiplication and addition. Check in which line it is first used.