PROOF 02
Prove.
a ÷ 0 cannot be defined
On the rationals ℚ. Two operations: + and ×.
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 b × x = a.
Proof.
Division asks multiplication in reverse. This definition places no condition on b.convention
∎
Lemma L1
For all a, a × 0 = 0
Proof.
(1)0 + 0 = 0A1
(2)a(0 + 0) = a × 0E
(3)a×0 + a×0 = a×0A6
(4)(a×0 + a×0) + (−(a×0)) = a×0 + (−(a×0))E
(5)a×0 + (a×0 + (−(a×0))) = 0A2, A3
(6)a × 0 = 0A3, A1
∎
Theorem T1
If a ≠ 0, then no x satisfies 0 × x = a.
Proof.
(1)Suppose such an x exists.assumption
(2)0 × x = x × 0A7
(3) = 0L1
(4)Therefore a = 0(1), (3), E
(5)This contradicts a ≠ 0.assumption
(6)No such x exists.(5)
∎
Theorem T2
The x satisfying 0 × x = 0 is not uniquely determined.
Proof.
(1)0 × 0 = 0A7, L1
(2)0 × 1 = 0A5, A7, L1
(3)0 ≠ 1A8
(4)There are two distinct solutions.(1), (2), (3)
∎
Corollary C
a ÷ 0 cannot be defined.
Proof.
(1)If a ≠ 0, there is no solution at all.T1
(2)If a = 0, the solution is not uniquely determined.T2
(3)In either case, D1 fails to assign a single value.D1, (1), (2)
∎
Remark
Can A8 be removed from this proof?
0 ≠ 1 looks too obvious to matter. Remove it and see what collapses.