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