Metamath Proof Explorer

Theorem irrdiff

Description: The irrationals are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 19-May-2024)

Ref Expression
Assertion irrdiff ⊢ A ∈ ℝ → ¬ A ∈ ℚ ↔ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r

Proof

Step Hyp Ref Expression
1 simplll ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ ∧ q ∈ ℚ ∧ r ∈ ℚ ∧ q ≠ r → A ∈ ℝ
2 simpllr ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ ∧ q ∈ ℚ ∧ r ∈ ℚ ∧ q ≠ r → ¬ A ∈ ℚ
3 simplrl ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ ∧ q ∈ ℚ ∧ r ∈ ℚ ∧ q ≠ r → q ∈ ℚ
4 simplrr ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ ∧ q ∈ ℚ ∧ r ∈ ℚ ∧ q ≠ r → r ∈ ℚ
5 simpr ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ ∧ q ∈ ℚ ∧ r ∈ ℚ ∧ q ≠ r → q ≠ r
6 1 2 3 4 5 irrdifflemf ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ ∧ q ∈ ℚ ∧ r ∈ ℚ ∧ q ≠ r → A − q ≠ A − r
7 6 ex ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ ∧ q ∈ ℚ ∧ r ∈ ℚ → q ≠ r → A − q ≠ A − r
8 7 ralrimivva ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ → ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r
9 simplr ⊢ A ∈ ℝ ∧ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r ∧ A ∈ ℚ → ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r
10 peano2rem ⊢ A ∈ ℝ → A − 1 ∈ ℝ
11 recn ⊢ A ∈ ℝ → A ∈ ℂ
12 1cnd ⊢ A ∈ ℝ → 1 ∈ ℂ
13 11 12 negsubd ⊢ A ∈ ℝ → A + -1 = A − 1
14 neg1lt0 ⊢ − 1 < 0
15 0lt1 ⊢ 0 < 1
16 neg1rr ⊢ − 1 ∈ ℝ
17 0re ⊢ 0 ∈ ℝ
18 1re ⊢ 1 ∈ ℝ
19 16 17 18 lttri ⊢ − 1 < 0 ∧ 0 < 1 → − 1 < 1
20 14 15 19 mp2an ⊢ − 1 < 1
21 16 a1i ⊢ A ∈ ℝ → − 1 ∈ ℝ
22 1red ⊢ A ∈ ℝ → 1 ∈ ℝ
23 id ⊢ A ∈ ℝ → A ∈ ℝ
24 21 22 23 ltadd2d ⊢ A ∈ ℝ → − 1 < 1 ↔ A + -1 < A + 1
25 20 24 mpbii ⊢ A ∈ ℝ → A + -1 < A + 1
26 13 25 eqbrtrrd ⊢ A ∈ ℝ → A − 1 < A + 1
27 10 26 ltned ⊢ A ∈ ℝ → A − 1 ≠ A + 1
28 27 ad2antrr ⊢ A ∈ ℝ ∧ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r ∧ A ∈ ℚ → A − 1 ≠ A + 1
29 1z ⊢ 1 ∈ ℤ
30 zq ⊢ 1 ∈ ℤ → 1 ∈ ℚ
31 29 30 ax-mp ⊢ 1 ∈ ℚ
32 qsubcl ⊢ A ∈ ℚ ∧ 1 ∈ ℚ → A − 1 ∈ ℚ
33 31 32 mpan2 ⊢ A ∈ ℚ → A − 1 ∈ ℚ
34 qaddcl ⊢ A ∈ ℚ ∧ 1 ∈ ℚ → A + 1 ∈ ℚ
35 31 34 mpan2 ⊢ A ∈ ℚ → A + 1 ∈ ℚ
36 35 adantl ⊢ A ∈ ℝ ∧ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r ∧ A ∈ ℚ → A + 1 ∈ ℚ
37 simpl ⊢ q = A − 1 ∧ r = A + 1 → q = A − 1
38 simpr ⊢ q = A − 1 ∧ r = A + 1 → r = A + 1
39 37 38 neeq12d ⊢ q = A − 1 ∧ r = A + 1 → q ≠ r ↔ A − 1 ≠ A + 1
40 oveq2 ⊢ q = A − 1 → A − q = A − A − 1
41 40 adantr ⊢ q = A − 1 ∧ r = A + 1 → A − q = A − A − 1
42 41 fveq2d ⊢ q = A − 1 ∧ r = A + 1 → A − q = A − A − 1
43 oveq2 ⊢ r = A + 1 → A − r = A − A + 1
44 43 adantl ⊢ q = A − 1 ∧ r = A + 1 → A − r = A − A + 1
45 44 fveq2d ⊢ q = A − 1 ∧ r = A + 1 → A − r = A − A + 1
46 42 45 neeq12d ⊢ q = A − 1 ∧ r = A + 1 → A − q ≠ A − r ↔ A − A − 1 ≠ A − A + 1
47 39 46 imbi12d ⊢ q = A − 1 ∧ r = A + 1 → q ≠ r → A − q ≠ A − r ↔ A − 1 ≠ A + 1 → A − A − 1 ≠ A − A + 1
48 47 rspc2gv ⊢ A − 1 ∈ ℚ ∧ A + 1 ∈ ℚ → ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r → A − 1 ≠ A + 1 → A − A − 1 ≠ A − A + 1
49 33 36 48 syl2an2 ⊢ A ∈ ℝ ∧ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r ∧ A ∈ ℚ → ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r → A − 1 ≠ A + 1 → A − A − 1 ≠ A − A + 1
50 9 28 49 mp2d ⊢ A ∈ ℝ ∧ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r ∧ A ∈ ℚ → A − A − 1 ≠ A − A + 1
51 neirr ⊢ ¬ 1 ≠ 1
52 11 12 nncand ⊢ A ∈ ℝ → A − A − 1 = 1
53 52 fveq2d ⊢ A ∈ ℝ → A − A − 1 = 1
54 11 12 subnegd ⊢ A ∈ ℝ → A − -1 = A + 1
55 54 oveq2d ⊢ A ∈ ℝ → A − A − -1 = A − A + 1
56 21 recnd ⊢ A ∈ ℝ → − 1 ∈ ℂ
57 11 56 nncand ⊢ A ∈ ℝ → A − A − -1 = − 1
58 55 57 eqtr3d ⊢ A ∈ ℝ → A − A + 1 = − 1
59 58 fveq2d ⊢ A ∈ ℝ → A − A + 1 = − 1
60 12 absnegd ⊢ A ∈ ℝ → − 1 = 1
61 59 60 eqtrd ⊢ A ∈ ℝ → A − A + 1 = 1
62 53 61 neeq12d ⊢ A ∈ ℝ → A − A − 1 ≠ A − A + 1 ↔ 1 ≠ 1
63 51 62 mtbiri ⊢ A ∈ ℝ → ¬ A − A − 1 ≠ A − A + 1
64 63 ad2antrr ⊢ A ∈ ℝ ∧ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r ∧ A ∈ ℚ → ¬ A − A − 1 ≠ A − A + 1
65 50 64 pm2.65da ⊢ A ∈ ℝ ∧ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r → ¬ A ∈ ℚ
66 8 65 impbida ⊢ A ∈ ℝ → ¬ A ∈ ℚ ↔ ∀ q ∈ ℚ ∀ r ∈ ℚ q ≠ r → A − q ≠ A − r