Metamath Proof Explorer

Theorem sqrt2irr

Description: The square root of 2 is irrational. See zsqrtelqelz for a generalization to all non-square integers. The proof's core is proven in sqrt2irrlem , which shows that if A / B = sqrt ( 2 ) , then A and B are even, so A / 2 and B / 2 are smaller representatives, which is absurd. An older version of this proof was included inThe Seventeen Provers of the World compiled by Freek Wiedijk. It is also the first of the "top 100" mathematical theorems whose formalization is tracked by Freek Wiedijk on hisFormalizing 100 Theorems page at http://www.cs.ru.nl/~freek/100/ . (Contributed by NM, 8-Jan-2002) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion sqrt2irr ⊢ 2 ∉ ℚ

Proof

Step Hyp Ref Expression
1 peano2nn ⊢ y ∈ ℕ → y + 1 ∈ ℕ
2 breq2 ⊢ n = 1 → z < n ↔ z < 1
3 2 imbi1d ⊢ n = 1 → z < n → ∀ x ∈ ℤ 2 ≠ x z ↔ z < 1 → ∀ x ∈ ℤ 2 ≠ x z
4 3 ralbidv ⊢ n = 1 → ∀ z ∈ ℕ z < n → ∀ x ∈ ℤ 2 ≠ x z ↔ ∀ z ∈ ℕ z < 1 → ∀ x ∈ ℤ 2 ≠ x z
5 breq2 ⊢ n = y → z < n ↔ z < y
6 5 imbi1d ⊢ n = y → z < n → ∀ x ∈ ℤ 2 ≠ x z ↔ z < y → ∀ x ∈ ℤ 2 ≠ x z
7 6 ralbidv ⊢ n = y → ∀ z ∈ ℕ z < n → ∀ x ∈ ℤ 2 ≠ x z ↔ ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z
8 breq2 ⊢ n = y + 1 → z < n ↔ z < y + 1
9 8 imbi1d ⊢ n = y + 1 → z < n → ∀ x ∈ ℤ 2 ≠ x z ↔ z < y + 1 → ∀ x ∈ ℤ 2 ≠ x z
10 9 ralbidv ⊢ n = y + 1 → ∀ z ∈ ℕ z < n → ∀ x ∈ ℤ 2 ≠ x z ↔ ∀ z ∈ ℕ z < y + 1 → ∀ x ∈ ℤ 2 ≠ x z
11 nnnlt1 ⊢ z ∈ ℕ → ¬ z < 1
12 11 pm2.21d ⊢ z ∈ ℕ → z < 1 → ∀ x ∈ ℤ 2 ≠ x z
13 12 rgen ⊢ ∀ z ∈ ℕ z < 1 → ∀ x ∈ ℤ 2 ≠ x z
14 nnrp ⊢ y ∈ ℕ → y ∈ ℝ +
15 rphalflt ⊢ y ∈ ℝ + → y 2 < y
16 14 15 syl ⊢ y ∈ ℕ → y 2 < y
17 breq1 ⊢ z = y 2 → z < y ↔ y 2 < y
18 oveq2 ⊢ z = y 2 → x z = x y 2
19 18 neeq2d ⊢ z = y 2 → 2 ≠ x z ↔ 2 ≠ x y 2
20 19 ralbidv ⊢ z = y 2 → ∀ x ∈ ℤ 2 ≠ x z ↔ ∀ x ∈ ℤ 2 ≠ x y 2
21 17 20 imbi12d ⊢ z = y 2 → z < y → ∀ x ∈ ℤ 2 ≠ x z ↔ y 2 < y → ∀ x ∈ ℤ 2 ≠ x y 2
22 21 rspcv ⊢ y 2 ∈ ℕ → ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z → y 2 < y → ∀ x ∈ ℤ 2 ≠ x y 2
23 22 com13 ⊢ y 2 < y → ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z → y 2 ∈ ℕ → ∀ x ∈ ℤ 2 ≠ x y 2
24 16 23 syl ⊢ y ∈ ℕ → ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z → y 2 ∈ ℕ → ∀ x ∈ ℤ 2 ≠ x y 2
25 simpr ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → 2 = z y
26 zcn ⊢ z ∈ ℤ → z ∈ ℂ
27 26 ad2antlr ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → z ∈ ℂ
28 nncn ⊢ y ∈ ℕ → y ∈ ℂ
29 28 ad2antrr ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → y ∈ ℂ
30 2cnd ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → 2 ∈ ℂ
31 nnne0 ⊢ y ∈ ℕ → y ≠ 0
32 31 ad2antrr ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → y ≠ 0
33 2ne0 ⊢ 2 ≠ 0
34 33 a1i ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → 2 ≠ 0
35 27 29 30 32 34 divcan7d ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → z 2 y 2 = z y
36 25 35 eqtr4d ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → 2 = z 2 y 2
37 simplr ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → z ∈ ℤ
38 simpll ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → y ∈ ℕ
39 37 38 25 sqrt2irrlem ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → z 2 ∈ ℤ ∧ y 2 ∈ ℕ
40 39 simprd ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → y 2 ∈ ℕ
41 39 simpld ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → z 2 ∈ ℤ
42 oveq1 ⊢ x = z 2 → x y 2 = z 2 y 2
43 42 neeq2d ⊢ x = z 2 → 2 ≠ x y 2 ↔ 2 ≠ z 2 y 2
44 43 rspcv ⊢ z 2 ∈ ℤ → ∀ x ∈ ℤ 2 ≠ x y 2 → 2 ≠ z 2 y 2
45 41 44 syl ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → ∀ x ∈ ℤ 2 ≠ x y 2 → 2 ≠ z 2 y 2
46 40 45 embantd ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → y 2 ∈ ℕ → ∀ x ∈ ℤ 2 ≠ x y 2 → 2 ≠ z 2 y 2
47 46 necon2bd ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → 2 = z 2 y 2 → ¬ y 2 ∈ ℕ → ∀ x ∈ ℤ 2 ≠ x y 2
48 36 47 mpd ⊢ y ∈ ℕ ∧ z ∈ ℤ ∧ 2 = z y → ¬ y 2 ∈ ℕ → ∀ x ∈ ℤ 2 ≠ x y 2
49 48 ex ⊢ y ∈ ℕ ∧ z ∈ ℤ → 2 = z y → ¬ y 2 ∈ ℕ → ∀ x ∈ ℤ 2 ≠ x y 2
50 49 necon2ad ⊢ y ∈ ℕ ∧ z ∈ ℤ → y 2 ∈ ℕ → ∀ x ∈ ℤ 2 ≠ x y 2 → 2 ≠ z y
51 50 ralrimdva ⊢ y ∈ ℕ → y 2 ∈ ℕ → ∀ x ∈ ℤ 2 ≠ x y 2 → ∀ z ∈ ℤ 2 ≠ z y
52 24 51 syld ⊢ y ∈ ℕ → ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z → ∀ z ∈ ℤ 2 ≠ z y
53 oveq1 ⊢ x = z → x y = z y
54 53 neeq2d ⊢ x = z → 2 ≠ x y ↔ 2 ≠ z y
55 54 cbvralvw ⊢ ∀ x ∈ ℤ 2 ≠ x y ↔ ∀ z ∈ ℤ 2 ≠ z y
56 52 55 syl6ibr ⊢ y ∈ ℕ → ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z → ∀ x ∈ ℤ 2 ≠ x y
57 oveq2 ⊢ z = y → x z = x y
58 57 neeq2d ⊢ z = y → 2 ≠ x z ↔ 2 ≠ x y
59 58 ralbidv ⊢ z = y → ∀ x ∈ ℤ 2 ≠ x z ↔ ∀ x ∈ ℤ 2 ≠ x y
60 59 ceqsralv ⊢ y ∈ ℕ → ∀ z ∈ ℕ z = y → ∀ x ∈ ℤ 2 ≠ x z ↔ ∀ x ∈ ℤ 2 ≠ x y
61 56 60 sylibrd ⊢ y ∈ ℕ → ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z → ∀ z ∈ ℕ z = y → ∀ x ∈ ℤ 2 ≠ x z
62 61 ancld ⊢ y ∈ ℕ → ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z → ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z ∧ ∀ z ∈ ℕ z = y → ∀ x ∈ ℤ 2 ≠ x z
63 nnleltp1 ⊢ z ∈ ℕ ∧ y ∈ ℕ → z ≤ y ↔ z < y + 1
64 nnre ⊢ z ∈ ℕ → z ∈ ℝ
65 nnre ⊢ y ∈ ℕ → y ∈ ℝ
66 leloe ⊢ z ∈ ℝ ∧ y ∈ ℝ → z ≤ y ↔ z < y ∨ z = y
67 64 65 66 syl2an ⊢ z ∈ ℕ ∧ y ∈ ℕ → z ≤ y ↔ z < y ∨ z = y
68 63 67 bitr3d ⊢ z ∈ ℕ ∧ y ∈ ℕ → z < y + 1 ↔ z < y ∨ z = y
69 68 ancoms ⊢ y ∈ ℕ ∧ z ∈ ℕ → z < y + 1 ↔ z < y ∨ z = y
70 69 imbi1d ⊢ y ∈ ℕ ∧ z ∈ ℕ → z < y + 1 → ∀ x ∈ ℤ 2 ≠ x z ↔ z < y ∨ z = y → ∀ x ∈ ℤ 2 ≠ x z
71 jaob ⊢ z < y ∨ z = y → ∀ x ∈ ℤ 2 ≠ x z ↔ z < y → ∀ x ∈ ℤ 2 ≠ x z ∧ z = y → ∀ x ∈ ℤ 2 ≠ x z
72 70 71 bitrdi ⊢ y ∈ ℕ ∧ z ∈ ℕ → z < y + 1 → ∀ x ∈ ℤ 2 ≠ x z ↔ z < y → ∀ x ∈ ℤ 2 ≠ x z ∧ z = y → ∀ x ∈ ℤ 2 ≠ x z
73 72 ralbidva ⊢ y ∈ ℕ → ∀ z ∈ ℕ z < y + 1 → ∀ x ∈ ℤ 2 ≠ x z ↔ ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z ∧ z = y → ∀ x ∈ ℤ 2 ≠ x z
74 r19.26 ⊢ ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z ∧ z = y → ∀ x ∈ ℤ 2 ≠ x z ↔ ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z ∧ ∀ z ∈ ℕ z = y → ∀ x ∈ ℤ 2 ≠ x z
75 73 74 bitrdi ⊢ y ∈ ℕ → ∀ z ∈ ℕ z < y + 1 → ∀ x ∈ ℤ 2 ≠ x z ↔ ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z ∧ ∀ z ∈ ℕ z = y → ∀ x ∈ ℤ 2 ≠ x z
76 62 75 sylibrd ⊢ y ∈ ℕ → ∀ z ∈ ℕ z < y → ∀ x ∈ ℤ 2 ≠ x z → ∀ z ∈ ℕ z < y + 1 → ∀ x ∈ ℤ 2 ≠ x z
77 4 7 10 10 13 76 nnind ⊢ y + 1 ∈ ℕ → ∀ z ∈ ℕ z < y + 1 → ∀ x ∈ ℤ 2 ≠ x z
78 1 77 syl ⊢ y ∈ ℕ → ∀ z ∈ ℕ z < y + 1 → ∀ x ∈ ℤ 2 ≠ x z
79 65 ltp1d ⊢ y ∈ ℕ → y < y + 1
80 breq1 ⊢ z = y → z < y + 1 ↔ y < y + 1
81 df-ne ⊢ 2 ≠ x y ↔ ¬ 2 = x y
82 58 81 bitrdi ⊢ z = y → 2 ≠ x z ↔ ¬ 2 = x y
83 82 ralbidv ⊢ z = y → ∀ x ∈ ℤ 2 ≠ x z ↔ ∀ x ∈ ℤ ¬ 2 = x y
84 ralnex ⊢ ∀ x ∈ ℤ ¬ 2 = x y ↔ ¬ ∃ x ∈ ℤ 2 = x y
85 83 84 bitrdi ⊢ z = y → ∀ x ∈ ℤ 2 ≠ x z ↔ ¬ ∃ x ∈ ℤ 2 = x y
86 80 85 imbi12d ⊢ z = y → z < y + 1 → ∀ x ∈ ℤ 2 ≠ x z ↔ y < y + 1 → ¬ ∃ x ∈ ℤ 2 = x y
87 86 rspcv ⊢ y ∈ ℕ → ∀ z ∈ ℕ z < y + 1 → ∀ x ∈ ℤ 2 ≠ x z → y < y + 1 → ¬ ∃ x ∈ ℤ 2 = x y
88 78 79 87 mp2d ⊢ y ∈ ℕ → ¬ ∃ x ∈ ℤ 2 = x y
89 88 nrex ⊢ ¬ ∃ y ∈ ℕ ∃ x ∈ ℤ 2 = x y
90 elq ⊢ 2 ∈ ℚ ↔ ∃ x ∈ ℤ ∃ y ∈ ℕ 2 = x y
91 rexcom ⊢ ∃ x ∈ ℤ ∃ y ∈ ℕ 2 = x y ↔ ∃ y ∈ ℕ ∃ x ∈ ℤ 2 = x y
92 90 91 bitri ⊢ 2 ∈ ℚ ↔ ∃ y ∈ ℕ ∃ x ∈ ℤ 2 = x y
93 89 92 mtbir ⊢ ¬ 2 ∈ ℚ
94 93 nelir ⊢ 2 ∉ ℚ