PROOF 09
Prove.
√2 is not rational
On the reals ℝ.
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.
If b ≠ 0, such an x is unique. With this notation, equations can be transformed without division.convention
∎
Definition D2
If an integer k exists with n = 2k, then n is even; if n = 2k + 1, then n is odd.
Proof.
Every integer is one of the two, and never both.A2
∎
Lemma L1
If n² is even, then n is even.
Proof.
(1)Suppose n is odd. n = 2k + 1assumption, D2
(2)n² = n(2k + 1)(1), E
(3) = n(2k) + nA7, A6
(4) = 2(nk) + (2k + 1)A4, A5, (1)
(5) = (2(nk) + 2k) + 1A3
(6) = 2(nk + k) + 1A7
(7)Therefore n² is odd.(6), D2
(8)If n² is even, n is not odd.(7), A2
(9)Therefore n is even.(8), A2
∎
Theorem T
No rational number x satisfies x² = 2.
Proof.
(1)Suppose such a rational x exists.assumption
(2)There are integers a, b with x = a/b, gcd(a, b) = 1.A1
(3)b × x = a(2), D1
(4)(bx)(bx) = a × a(3), E
(5)(bx)(bx) = (b × b)(x × x)A4, A5
(6)b²x² = a²(4), (5)
(7)x² = 2(1)
(8)2b² = a²(6), (7), A5
(9)a² is even.(8), D2
(10)a is even. a = 2k(9), L1, D2
(11)a² = (2k)(2k) = 2(2k²)(10), E, A4, A5
(12)2b² = 2(2k²)(8), (11)
(13)b² = 2k²(12), A8
(14)b² is even.(13), D2
(15)b is even as well.(14), L1
(16)a and b are both divisible by 2.(10), (15)
(17)This contradicts gcd(a, b) = 1.(2), (16)
(18)No such x exists.(17)
∎
Remark
Can A1 be removed from this proof?
The contradiction detonates in the last line. Check what that contradiction rests on.