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 e. RR -> ( -. A e. QQ <-> A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simplll 
 |-  ( ( ( ( A e. RR /\ -. A e. QQ ) /\ ( q e. QQ /\ r e. QQ ) ) /\ q =/= r ) -> A e. RR )
2 simpllr 
 |-  ( ( ( ( A e. RR /\ -. A e. QQ ) /\ ( q e. QQ /\ r e. QQ ) ) /\ q =/= r ) -> -. A e. QQ )
3 simplrl 
 |-  ( ( ( ( A e. RR /\ -. A e. QQ ) /\ ( q e. QQ /\ r e. QQ ) ) /\ q =/= r ) -> q e. QQ )
4 simplrr 
 |-  ( ( ( ( A e. RR /\ -. A e. QQ ) /\ ( q e. QQ /\ r e. QQ ) ) /\ q =/= r ) -> r e. QQ )
5 simpr 
 |-  ( ( ( ( A e. RR /\ -. A e. QQ ) /\ ( q e. QQ /\ r e. QQ ) ) /\ q =/= r ) -> q =/= r )
6 1 2 3 4 5 irrdifflemf 
 |-  ( ( ( ( A e. RR /\ -. A e. QQ ) /\ ( q e. QQ /\ r e. QQ ) ) /\ q =/= r ) -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) )
7 6 ex 
 |-  ( ( ( A e. RR /\ -. A e. QQ ) /\ ( q e. QQ /\ r e. QQ ) ) -> ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) )
8 7 ralrimivva 
 |-  ( ( A e. RR /\ -. A e. QQ ) -> A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) )
9 simplr 
 |-  ( ( ( A e. RR /\ A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) ) /\ A e. QQ ) -> A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) )
10 peano2rem 
 |-  ( A e. RR -> ( A - 1 ) e. RR )
11 recn 
 |-  ( A e. RR -> A e. CC )
12 1cnd 
 |-  ( A e. RR -> 1 e. CC )
13 11 12 negsubd 
 |-  ( A e. RR -> ( A + -u 1 ) = ( A - 1 ) )
14 neg1lt0 
 |-  -u 1 < 0
15 0lt1 
 |-  0 < 1
16 neg1rr 
 |-  -u 1 e. RR
17 0re 
 |-  0 e. RR
18 1re 
 |-  1 e. RR
19 16 17 18 lttri 
 |-  ( ( -u 1 < 0 /\ 0 < 1 ) -> -u 1 < 1 )
20 14 15 19 mp2an 
 |-  -u 1 < 1
21 16 a1i 
 |-  ( A e. RR -> -u 1 e. RR )
22 1red 
 |-  ( A e. RR -> 1 e. RR )
23 id 
 |-  ( A e. RR -> A e. RR )
24 21 22 23 ltadd2d 
 |-  ( A e. RR -> ( -u 1 < 1 <-> ( A + -u 1 ) < ( A + 1 ) ) )
25 20 24 mpbii 
 |-  ( A e. RR -> ( A + -u 1 ) < ( A + 1 ) )
26 13 25 eqbrtrrd 
 |-  ( A e. RR -> ( A - 1 ) < ( A + 1 ) )
27 10 26 ltned 
 |-  ( A e. RR -> ( A - 1 ) =/= ( A + 1 ) )
28 27 ad2antrr 
 |-  ( ( ( A e. RR /\ A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) ) /\ A e. QQ ) -> ( A - 1 ) =/= ( A + 1 ) )
29 1z 
 |-  1 e. ZZ
30 zq 
 |-  ( 1 e. ZZ -> 1 e. QQ )
31 29 30 ax-mp 
 |-  1 e. QQ
32 qsubcl 
 |-  ( ( A e. QQ /\ 1 e. QQ ) -> ( A - 1 ) e. QQ )
33 31 32 mpan2 
 |-  ( A e. QQ -> ( A - 1 ) e. QQ )
34 qaddcl 
 |-  ( ( A e. QQ /\ 1 e. QQ ) -> ( A + 1 ) e. QQ )
35 31 34 mpan2 
 |-  ( A e. QQ -> ( A + 1 ) e. QQ )
36 35 adantl 
 |-  ( ( ( A e. RR /\ A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) ) /\ A e. QQ ) -> ( A + 1 ) e. QQ )
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 ) ) -> ( abs ` ( A - q ) ) = ( abs ` ( 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 ) ) -> ( abs ` ( A - r ) ) = ( abs ` ( A - ( A + 1 ) ) ) )
46 42 45 neeq12d 
 |-  ( ( q = ( A - 1 ) /\ r = ( A + 1 ) ) -> ( ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) <-> ( abs ` ( A - ( A - 1 ) ) ) =/= ( abs ` ( A - ( A + 1 ) ) ) ) )
47 39 46 imbi12d 
 |-  ( ( q = ( A - 1 ) /\ r = ( A + 1 ) ) -> ( ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) <-> ( ( A - 1 ) =/= ( A + 1 ) -> ( abs ` ( A - ( A - 1 ) ) ) =/= ( abs ` ( A - ( A + 1 ) ) ) ) ) )
48 47 rspc2gv 
 |-  ( ( ( A - 1 ) e. QQ /\ ( A + 1 ) e. QQ ) -> ( A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) -> ( ( A - 1 ) =/= ( A + 1 ) -> ( abs ` ( A - ( A - 1 ) ) ) =/= ( abs ` ( A - ( A + 1 ) ) ) ) ) )
49 33 36 48 syl2an2 
 |-  ( ( ( A e. RR /\ A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) ) /\ A e. QQ ) -> ( A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) -> ( ( A - 1 ) =/= ( A + 1 ) -> ( abs ` ( A - ( A - 1 ) ) ) =/= ( abs ` ( A - ( A + 1 ) ) ) ) ) )
50 9 28 49 mp2d 
 |-  ( ( ( A e. RR /\ A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) ) /\ A e. QQ ) -> ( abs ` ( A - ( A - 1 ) ) ) =/= ( abs ` ( A - ( A + 1 ) ) ) )
51 neirr 
 |-  -. ( abs ` 1 ) =/= ( abs ` 1 )
52 11 12 nncand 
 |-  ( A e. RR -> ( A - ( A - 1 ) ) = 1 )
53 52 fveq2d 
 |-  ( A e. RR -> ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` 1 ) )
54 11 12 subnegd 
 |-  ( A e. RR -> ( A - -u 1 ) = ( A + 1 ) )
55 54 oveq2d 
 |-  ( A e. RR -> ( A - ( A - -u 1 ) ) = ( A - ( A + 1 ) ) )
56 21 recnd 
 |-  ( A e. RR -> -u 1 e. CC )
57 11 56 nncand 
 |-  ( A e. RR -> ( A - ( A - -u 1 ) ) = -u 1 )
58 55 57 eqtr3d 
 |-  ( A e. RR -> ( A - ( A + 1 ) ) = -u 1 )
59 58 fveq2d 
 |-  ( A e. RR -> ( abs ` ( A - ( A + 1 ) ) ) = ( abs ` -u 1 ) )
60 12 absnegd 
 |-  ( A e. RR -> ( abs ` -u 1 ) = ( abs ` 1 ) )
61 59 60 eqtrd 
 |-  ( A e. RR -> ( abs ` ( A - ( A + 1 ) ) ) = ( abs ` 1 ) )
62 53 61 neeq12d 
 |-  ( A e. RR -> ( ( abs ` ( A - ( A - 1 ) ) ) =/= ( abs ` ( A - ( A + 1 ) ) ) <-> ( abs ` 1 ) =/= ( abs ` 1 ) ) )
63 51 62 mtbiri 
 |-  ( A e. RR -> -. ( abs ` ( A - ( A - 1 ) ) ) =/= ( abs ` ( A - ( A + 1 ) ) ) )
64 63 ad2antrr 
 |-  ( ( ( A e. RR /\ A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) ) /\ A e. QQ ) -> -. ( abs ` ( A - ( A - 1 ) ) ) =/= ( abs ` ( A - ( A + 1 ) ) ) )
65 50 64 pm2.65da 
 |-  ( ( A e. RR /\ A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) ) -> -. A e. QQ )
66 8 65 impbida 
 |-  ( A e. RR -> ( -. A e. QQ <-> A. q e. QQ A. r e. QQ ( q =/= r -> ( abs ` ( A - q ) ) =/= ( abs ` ( A - r ) ) ) ) )