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