MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sqrt2irr Structured version   Visualization version   GIF version

Theorem sqrt2irr 16189
Description: The square root of 2 is irrational. See zsqrtelqelz 16691 for a generalization to all non-square integers. The proof's core is proven in sqrt2irrlem 16188, which shows that if 𝐴 / 𝐵 = √(2), then 𝐴 and 𝐵 are even, so 𝐴 / 2 and 𝐵 / 2 are smaller representatives, which is absurd. An older version of this proof was included in The 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 his Formalizing 100 Theorems page at http://www.cs.ru.nl/~freek/100/ 16188. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
Assertion
Ref Expression
sqrt2irr (√‘2) ∉ ℚ

Proof of Theorem sqrt2irr
Dummy variables 𝑥 𝑛 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano2nn 12221 . . . . . 6 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
2 breq2 5152 . . . . . . . . 9 (𝑛 = 1 → (𝑧 < 𝑛𝑧 < 1))
32imbi1d 342 . . . . . . . 8 (𝑛 = 1 → ((𝑧 < 𝑛 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ (𝑧 < 1 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))))
43ralbidv 3178 . . . . . . 7 (𝑛 = 1 → (∀𝑧 ∈ ℕ (𝑧 < 𝑛 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ ∀𝑧 ∈ ℕ (𝑧 < 1 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))))
5 breq2 5152 . . . . . . . . 9 (𝑛 = 𝑦 → (𝑧 < 𝑛𝑧 < 𝑦))
65imbi1d 342 . . . . . . . 8 (𝑛 = 𝑦 → ((𝑧 < 𝑛 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))))
76ralbidv 3178 . . . . . . 7 (𝑛 = 𝑦 → (∀𝑧 ∈ ℕ (𝑧 < 𝑛 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ ∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))))
8 breq2 5152 . . . . . . . . 9 (𝑛 = (𝑦 + 1) → (𝑧 < 𝑛𝑧 < (𝑦 + 1)))
98imbi1d 342 . . . . . . . 8 (𝑛 = (𝑦 + 1) → ((𝑧 < 𝑛 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ (𝑧 < (𝑦 + 1) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))))
109ralbidv 3178 . . . . . . 7 (𝑛 = (𝑦 + 1) → (∀𝑧 ∈ ℕ (𝑧 < 𝑛 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))))
11 nnnlt1 12241 . . . . . . . . 9 (𝑧 ∈ ℕ → ¬ 𝑧 < 1)
1211pm2.21d 121 . . . . . . . 8 (𝑧 ∈ ℕ → (𝑧 < 1 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)))
1312rgen 3064 . . . . . . 7 𝑧 ∈ ℕ (𝑧 < 1 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))
14 nnrp 12982 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ+)
15 rphalflt 13000 . . . . . . . . . . . . . 14 (𝑦 ∈ ℝ+ → (𝑦 / 2) < 𝑦)
1614, 15syl 17 . . . . . . . . . . . . 13 (𝑦 ∈ ℕ → (𝑦 / 2) < 𝑦)
17 breq1 5151 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑦 / 2) → (𝑧 < 𝑦 ↔ (𝑦 / 2) < 𝑦))
18 oveq2 7414 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦 / 2) → (𝑥 / 𝑧) = (𝑥 / (𝑦 / 2)))
1918neeq2d 3002 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦 / 2) → ((√‘2) ≠ (𝑥 / 𝑧) ↔ (√‘2) ≠ (𝑥 / (𝑦 / 2))))
2019ralbidv 3178 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑦 / 2) → (∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧) ↔ ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2))))
2117, 20imbi12d 345 . . . . . . . . . . . . . . 15 (𝑧 = (𝑦 / 2) → ((𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ ((𝑦 / 2) < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2)))))
2221rspcv 3609 . . . . . . . . . . . . . 14 ((𝑦 / 2) ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) → ((𝑦 / 2) < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2)))))
2322com13 88 . . . . . . . . . . . . 13 ((𝑦 / 2) < 𝑦 → (∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) → ((𝑦 / 2) ∈ ℕ → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2)))))
2416, 23syl 17 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) → ((𝑦 / 2) ∈ ℕ → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2)))))
25 simpr 486 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → (√‘2) = (𝑧 / 𝑦))
26 zcn 12560 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℤ → 𝑧 ∈ ℂ)
2726ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → 𝑧 ∈ ℂ)
28 nncn 12217 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
2928ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → 𝑦 ∈ ℂ)
30 2cnd 12287 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → 2 ∈ ℂ)
31 nnne0 12243 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ → 𝑦 ≠ 0)
3231ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → 𝑦 ≠ 0)
33 2ne0 12313 . . . . . . . . . . . . . . . . . . 19 2 ≠ 0
3433a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → 2 ≠ 0)
3527, 29, 30, 32, 34divcan7d 12015 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → ((𝑧 / 2) / (𝑦 / 2)) = (𝑧 / 𝑦))
3625, 35eqtr4d 2776 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → (√‘2) = ((𝑧 / 2) / (𝑦 / 2)))
37 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → 𝑧 ∈ ℤ)
38 simpll 766 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → 𝑦 ∈ ℕ)
3937, 38, 25sqrt2irrlem 16188 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → ((𝑧 / 2) ∈ ℤ ∧ (𝑦 / 2) ∈ ℕ))
4039simprd 497 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → (𝑦 / 2) ∈ ℕ)
4139simpld 496 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → (𝑧 / 2) ∈ ℤ)
42 oveq1 7413 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑧 / 2) → (𝑥 / (𝑦 / 2)) = ((𝑧 / 2) / (𝑦 / 2)))
4342neeq2d 3002 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑧 / 2) → ((√‘2) ≠ (𝑥 / (𝑦 / 2)) ↔ (√‘2) ≠ ((𝑧 / 2) / (𝑦 / 2))))
4443rspcv 3609 . . . . . . . . . . . . . . . . . . 19 ((𝑧 / 2) ∈ ℤ → (∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2)) → (√‘2) ≠ ((𝑧 / 2) / (𝑦 / 2))))
4541, 44syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → (∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2)) → (√‘2) ≠ ((𝑧 / 2) / (𝑦 / 2))))
4640, 45embantd 59 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → (((𝑦 / 2) ∈ ℕ → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2))) → (√‘2) ≠ ((𝑧 / 2) / (𝑦 / 2))))
4746necon2bd 2957 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → ((√‘2) = ((𝑧 / 2) / (𝑦 / 2)) → ¬ ((𝑦 / 2) ∈ ℕ → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2)))))
4836, 47mpd 15 . . . . . . . . . . . . . . 15 (((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) ∧ (√‘2) = (𝑧 / 𝑦)) → ¬ ((𝑦 / 2) ∈ ℕ → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2))))
4948ex 414 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → ((√‘2) = (𝑧 / 𝑦) → ¬ ((𝑦 / 2) ∈ ℕ → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2)))))
5049necon2ad 2956 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℤ) → (((𝑦 / 2) ∈ ℕ → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2))) → (√‘2) ≠ (𝑧 / 𝑦)))
5150ralrimdva 3155 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → (((𝑦 / 2) ∈ ℕ → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / (𝑦 / 2))) → ∀𝑧 ∈ ℤ (√‘2) ≠ (𝑧 / 𝑦)))
5224, 51syld 47 . . . . . . . . . . 11 (𝑦 ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) → ∀𝑧 ∈ ℤ (√‘2) ≠ (𝑧 / 𝑦)))
53 oveq1 7413 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥 / 𝑦) = (𝑧 / 𝑦))
5453neeq2d 3002 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((√‘2) ≠ (𝑥 / 𝑦) ↔ (√‘2) ≠ (𝑧 / 𝑦)))
5554cbvralvw 3235 . . . . . . . . . . 11 (∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑦) ↔ ∀𝑧 ∈ ℤ (√‘2) ≠ (𝑧 / 𝑦))
5652, 55syl6ibr 252 . . . . . . . . . 10 (𝑦 ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑦)))
57 oveq2 7414 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑥 / 𝑧) = (𝑥 / 𝑦))
5857neeq2d 3002 . . . . . . . . . . . 12 (𝑧 = 𝑦 → ((√‘2) ≠ (𝑥 / 𝑧) ↔ (√‘2) ≠ (𝑥 / 𝑦)))
5958ralbidv 3178 . . . . . . . . . . 11 (𝑧 = 𝑦 → (∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧) ↔ ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑦)))
6059ceqsralv 3514 . . . . . . . . . 10 (𝑦 ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 = 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑦)))
6156, 60sylibrd 259 . . . . . . . . 9 (𝑦 ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) → ∀𝑧 ∈ ℕ (𝑧 = 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))))
6261ancld 552 . . . . . . . 8 (𝑦 ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) → (∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ∧ ∀𝑧 ∈ ℕ (𝑧 = 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)))))
63 nnleltp1 12614 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑧𝑦𝑧 < (𝑦 + 1)))
64 nnre 12216 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℕ → 𝑧 ∈ ℝ)
65 nnre 12216 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
66 leloe 11297 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑧𝑦 ↔ (𝑧 < 𝑦𝑧 = 𝑦)))
6764, 65, 66syl2an 597 . . . . . . . . . . . . . 14 ((𝑧 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑧𝑦 ↔ (𝑧 < 𝑦𝑧 = 𝑦)))
6863, 67bitr3d 281 . . . . . . . . . . . . 13 ((𝑧 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑧 < (𝑦 + 1) ↔ (𝑧 < 𝑦𝑧 = 𝑦)))
6968ancoms 460 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑧 < (𝑦 + 1) ↔ (𝑧 < 𝑦𝑧 = 𝑦)))
7069imbi1d 342 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧 < (𝑦 + 1) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ ((𝑧 < 𝑦𝑧 = 𝑦) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))))
71 jaob 961 . . . . . . . . . . 11 (((𝑧 < 𝑦𝑧 = 𝑦) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ ((𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ∧ (𝑧 = 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))))
7270, 71bitrdi 287 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((𝑧 < (𝑦 + 1) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ ((𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ∧ (𝑧 = 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)))))
7372ralbidva 3176 . . . . . . . . 9 (𝑦 ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ ∀𝑧 ∈ ℕ ((𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ∧ (𝑧 = 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)))))
74 r19.26 3112 . . . . . . . . 9 (∀𝑧 ∈ ℕ ((𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ∧ (𝑧 = 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))) ↔ (∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ∧ ∀𝑧 ∈ ℕ (𝑧 = 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))))
7573, 74bitrdi 287 . . . . . . . 8 (𝑦 ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ (∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ∧ ∀𝑧 ∈ ℕ (𝑧 = 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)))))
7662, 75sylibrd 259 . . . . . . 7 (𝑦 ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 < 𝑦 → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) → ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧))))
774, 7, 10, 10, 13, 76nnind 12227 . . . . . 6 ((𝑦 + 1) ∈ ℕ → ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)))
781, 77syl 17 . . . . 5 (𝑦 ∈ ℕ → ∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)))
7965ltp1d 12141 . . . . 5 (𝑦 ∈ ℕ → 𝑦 < (𝑦 + 1))
80 breq1 5151 . . . . . . 7 (𝑧 = 𝑦 → (𝑧 < (𝑦 + 1) ↔ 𝑦 < (𝑦 + 1)))
81 df-ne 2942 . . . . . . . . . 10 ((√‘2) ≠ (𝑥 / 𝑦) ↔ ¬ (√‘2) = (𝑥 / 𝑦))
8258, 81bitrdi 287 . . . . . . . . 9 (𝑧 = 𝑦 → ((√‘2) ≠ (𝑥 / 𝑧) ↔ ¬ (√‘2) = (𝑥 / 𝑦)))
8382ralbidv 3178 . . . . . . . 8 (𝑧 = 𝑦 → (∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧) ↔ ∀𝑥 ∈ ℤ ¬ (√‘2) = (𝑥 / 𝑦)))
84 ralnex 3073 . . . . . . . 8 (∀𝑥 ∈ ℤ ¬ (√‘2) = (𝑥 / 𝑦) ↔ ¬ ∃𝑥 ∈ ℤ (√‘2) = (𝑥 / 𝑦))
8583, 84bitrdi 287 . . . . . . 7 (𝑧 = 𝑦 → (∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧) ↔ ¬ ∃𝑥 ∈ ℤ (√‘2) = (𝑥 / 𝑦)))
8680, 85imbi12d 345 . . . . . 6 (𝑧 = 𝑦 → ((𝑧 < (𝑦 + 1) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) ↔ (𝑦 < (𝑦 + 1) → ¬ ∃𝑥 ∈ ℤ (√‘2) = (𝑥 / 𝑦))))
8786rspcv 3609 . . . . 5 (𝑦 ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 < (𝑦 + 1) → ∀𝑥 ∈ ℤ (√‘2) ≠ (𝑥 / 𝑧)) → (𝑦 < (𝑦 + 1) → ¬ ∃𝑥 ∈ ℤ (√‘2) = (𝑥 / 𝑦))))
8878, 79, 87mp2d 49 . . . 4 (𝑦 ∈ ℕ → ¬ ∃𝑥 ∈ ℤ (√‘2) = (𝑥 / 𝑦))
8988nrex 3075 . . 3 ¬ ∃𝑦 ∈ ℕ ∃𝑥 ∈ ℤ (√‘2) = (𝑥 / 𝑦)
90 elq 12931 . . . 4 ((√‘2) ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (√‘2) = (𝑥 / 𝑦))
91 rexcom 3288 . . . 4 (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (√‘2) = (𝑥 / 𝑦) ↔ ∃𝑦 ∈ ℕ ∃𝑥 ∈ ℤ (√‘2) = (𝑥 / 𝑦))
9290, 91bitri 275 . . 3 ((√‘2) ∈ ℚ ↔ ∃𝑦 ∈ ℕ ∃𝑥 ∈ ℤ (√‘2) = (𝑥 / 𝑦))
9389, 92mtbir 323 . 2 ¬ (√‘2) ∈ ℚ
9493nelir 3050 1 (√‘2) ∉ ℚ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846   = wceq 1542  wcel 2107  wne 2941  wnel 3047  wral 3062  wrex 3071   class class class wbr 5148  cfv 6541  (class class class)co 7406  cc 11105  cr 11106  0cc0 11107  1c1 11108   + caddc 11110   < clt 11245  cle 11246   / cdiv 11868  cn 12209  2c2 12264  cz 12555  cq 12929  +crp 12971  csqrt 15177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-sup 9434  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-seq 13964  df-exp 14025  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180
This theorem is referenced by:  sqrt2irr0  16191  nthruc  16192  2sq2  26926
  Copyright terms: Public domain W3C validator