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 ( 𝐴 ∈ ℝ → ( ¬ 𝐴 ∈ ℚ ↔ ∀ 𝑞 ∈ ℚ ∀ 𝑟 ∈ ℚ ( 𝑞 ≠ 𝑟 → ( abs ‘ ( 𝐴 − 𝑞 ) ) ≠ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) )

Proof

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