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