Metamath Proof Explorer

Theorem qdiff

Description: The rationals are exactly those reals for which there exist two distinct rationals that are the same distance from the original number. Similar to irrdiff but here proved with a proof which would also work in constructive mathematics. From an online post by Ingo Blechschmidt. For a proof using irrdiff , see qdiffALT . (Contributed by Jim Kingdon, 24-Apr-2026)

Ref Expression
Assertion qdiff 
|- ( A e. RR -> ( A e. QQ <-> E. q e. QQ E. r e. QQ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) )

Proof

Step Hyp Ref Expression
1 neeq1 
 |-  ( q = ( A - 1 ) -> ( q =/= r <-> ( A - 1 ) =/= r ) )
2 oveq2 
 |-  ( q = ( A - 1 ) -> ( A - q ) = ( A - ( A - 1 ) ) )
3 2 fveqeq2d 
 |-  ( q = ( A - 1 ) -> ( ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) <-> ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` ( A - r ) ) ) )
4 1 3 anbi12d 
 |-  ( q = ( A - 1 ) -> ( ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) <-> ( ( A - 1 ) =/= r /\ ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` ( A - r ) ) ) ) )
5 4 rexbidv 
 |-  ( q = ( A - 1 ) -> ( E. r e. QQ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) <-> E. r e. QQ ( ( A - 1 ) =/= r /\ ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` ( A - r ) ) ) ) )
6 1z 
 |-  1 e. ZZ
7 zq 
 |-  ( 1 e. ZZ -> 1 e. QQ )
8 6 7 ax-mp 
 |-  1 e. QQ
9 qsubcl 
 |-  ( ( A e. QQ /\ 1 e. QQ ) -> ( A - 1 ) e. QQ )
10 8 9 mpan2 
 |-  ( A e. QQ -> ( A - 1 ) e. QQ )
11 qaddcl 
 |-  ( ( A e. QQ /\ 1 e. QQ ) -> ( A + 1 ) e. QQ )
12 8 11 mpan2 
 |-  ( A e. QQ -> ( A + 1 ) e. QQ )
13 qre 
 |-  ( A e. QQ -> A e. RR )
14 1rp 
 |-  1 e. RR+
15 14 14 pm3.2i 
 |-  ( 1 e. RR+ /\ 1 e. RR+ )
16 rpaddcl 
 |-  ( ( 1 e. RR+ /\ 1 e. RR+ ) -> ( 1 + 1 ) e. RR+ )
17 15 16 mp1i 
 |-  ( A e. QQ -> ( 1 + 1 ) e. RR+ )
18 13 17 ltaddrpd 
 |-  ( A e. QQ -> A < ( A + ( 1 + 1 ) ) )
19 13 18 ltned 
 |-  ( A e. QQ -> A =/= ( A + ( 1 + 1 ) ) )
20 19 neneqd 
 |-  ( A e. QQ -> -. A = ( A + ( 1 + 1 ) ) )
21 20 neqcomd 
 |-  ( A e. QQ -> -. ( A + ( 1 + 1 ) ) = A )
22 qcn 
 |-  ( A e. QQ -> A e. CC )
23 1cnd 
 |-  ( A e. QQ -> 1 e. CC )
24 22 23 23 addassd 
 |-  ( A e. QQ -> ( ( A + 1 ) + 1 ) = ( A + ( 1 + 1 ) ) )
25 24 eqeq1d 
 |-  ( A e. QQ -> ( ( ( A + 1 ) + 1 ) = A <-> ( A + ( 1 + 1 ) ) = A ) )
26 21 25 mtbird 
 |-  ( A e. QQ -> -. ( ( A + 1 ) + 1 ) = A )
27 22 23 addcld 
 |-  ( A e. QQ -> ( A + 1 ) e. CC )
28 22 23 27 subadd2d 
 |-  ( A e. QQ -> ( ( A - 1 ) = ( A + 1 ) <-> ( ( A + 1 ) + 1 ) = A ) )
29 26 28 mtbird 
 |-  ( A e. QQ -> -. ( A - 1 ) = ( A + 1 ) )
30 29 neqned 
 |-  ( A e. QQ -> ( A - 1 ) =/= ( A + 1 ) )
31 23 absnegd 
 |-  ( A e. QQ -> ( abs ` -u 1 ) = ( abs ` 1 ) )
32 22 22 23 subsub4d 
 |-  ( A e. QQ -> ( ( A - A ) - 1 ) = ( A - ( A + 1 ) ) )
33 22 subidd 
 |-  ( A e. QQ -> ( A - A ) = 0 )
34 33 oveq1d 
 |-  ( A e. QQ -> ( ( A - A ) - 1 ) = ( 0 - 1 ) )
35 df-neg 
 |-  -u 1 = ( 0 - 1 )
36 34 35 eqtr4di 
 |-  ( A e. QQ -> ( ( A - A ) - 1 ) = -u 1 )
37 32 36 eqtr3d 
 |-  ( A e. QQ -> ( A - ( A + 1 ) ) = -u 1 )
38 37 fveq2d 
 |-  ( A e. QQ -> ( abs ` ( A - ( A + 1 ) ) ) = ( abs ` -u 1 ) )
39 22 23 nncand 
 |-  ( A e. QQ -> ( A - ( A - 1 ) ) = 1 )
40 39 fveq2d 
 |-  ( A e. QQ -> ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` 1 ) )
41 31 38 40 3eqtr4rd 
 |-  ( A e. QQ -> ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` ( A - ( A + 1 ) ) ) )
42 neeq2 
 |-  ( r = ( A + 1 ) -> ( ( A - 1 ) =/= r <-> ( A - 1 ) =/= ( A + 1 ) ) )
43 oveq2 
 |-  ( r = ( A + 1 ) -> ( A - r ) = ( A - ( A + 1 ) ) )
44 43 fveq2d 
 |-  ( r = ( A + 1 ) -> ( abs ` ( A - r ) ) = ( abs ` ( A - ( A + 1 ) ) ) )
45 44 eqeq2d 
 |-  ( r = ( A + 1 ) -> ( ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` ( A - r ) ) <-> ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` ( A - ( A + 1 ) ) ) ) )
46 42 45 anbi12d 
 |-  ( r = ( A + 1 ) -> ( ( ( A - 1 ) =/= r /\ ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` ( A - r ) ) ) <-> ( ( A - 1 ) =/= ( A + 1 ) /\ ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` ( A - ( A + 1 ) ) ) ) ) )
47 46 rspcev 
 |-  ( ( ( A + 1 ) e. QQ /\ ( ( A - 1 ) =/= ( A + 1 ) /\ ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` ( A - ( A + 1 ) ) ) ) ) -> E. r e. QQ ( ( A - 1 ) =/= r /\ ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` ( A - r ) ) ) )
48 12 30 41 47 syl12anc 
 |-  ( A e. QQ -> E. r e. QQ ( ( A - 1 ) =/= r /\ ( abs ` ( A - ( A - 1 ) ) ) = ( abs ` ( A - r ) ) ) )
49 5 10 48 rspcedvdw 
 |-  ( A e. QQ -> E. q e. QQ E. r e. QQ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) )
50 2cnd 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> 2 e. CC )
51 simpll 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> A e. RR )
52 51 recnd 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> A e. CC )
53 simplrl 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> q e. QQ )
54 53 qred 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> q e. RR )
55 54 recnd 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> q e. CC )
56 52 55 mulcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( A x. q ) e. CC )
57 simplrr 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> r e. QQ )
58 57 qred 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> r e. RR )
59 58 recnd 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> r e. CC )
60 52 59 mulcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( A x. r ) e. CC )
61 50 56 60 subdid 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( 2 x. ( ( A x. q ) - ( A x. r ) ) ) = ( ( 2 x. ( A x. q ) ) - ( 2 x. ( A x. r ) ) ) )
62 52 sqcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( A ^ 2 ) e. CC )
63 50 60 mulcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( 2 x. ( A x. r ) ) e. CC )
64 50 56 mulcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( 2 x. ( A x. q ) ) e. CC )
65 62 63 64 nnncan1d 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( A ^ 2 ) - ( 2 x. ( A x. r ) ) ) - ( ( A ^ 2 ) - ( 2 x. ( A x. q ) ) ) ) = ( ( 2 x. ( A x. q ) ) - ( 2 x. ( A x. r ) ) ) )
66 simprr 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) )
67 51 54 resubcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( A - q ) e. RR )
68 51 58 resubcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( A - r ) e. RR )
69 sqabs 
 |-  ( ( ( A - q ) e. RR /\ ( A - r ) e. RR ) -> ( ( ( A - q ) ^ 2 ) = ( ( A - r ) ^ 2 ) <-> ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) )
70 67 68 69 syl2anc 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( A - q ) ^ 2 ) = ( ( A - r ) ^ 2 ) <-> ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) )
71 66 70 mpbird 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( A - q ) ^ 2 ) = ( ( A - r ) ^ 2 ) )
72 binom2sub 
 |-  ( ( A e. CC /\ q e. CC ) -> ( ( A - q ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. q ) ) ) + ( q ^ 2 ) ) )
73 52 55 72 syl2anc 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( A - q ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. q ) ) ) + ( q ^ 2 ) ) )
74 binom2sub 
 |-  ( ( A e. CC /\ r e. CC ) -> ( ( A - r ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. r ) ) ) + ( r ^ 2 ) ) )
75 52 59 74 syl2anc 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( A - r ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. r ) ) ) + ( r ^ 2 ) ) )
76 71 73 75 3eqtr3d 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( A ^ 2 ) - ( 2 x. ( A x. q ) ) ) + ( q ^ 2 ) ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. r ) ) ) + ( r ^ 2 ) ) )
77 62 64 subcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( A ^ 2 ) - ( 2 x. ( A x. q ) ) ) e. CC )
78 55 sqcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( q ^ 2 ) e. CC )
79 62 63 subcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( A ^ 2 ) - ( 2 x. ( A x. r ) ) ) e. CC )
80 59 sqcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( r ^ 2 ) e. CC )
81 77 78 79 80 addsubeq4d 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( ( A ^ 2 ) - ( 2 x. ( A x. q ) ) ) + ( q ^ 2 ) ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. r ) ) ) + ( r ^ 2 ) ) <-> ( ( ( A ^ 2 ) - ( 2 x. ( A x. r ) ) ) - ( ( A ^ 2 ) - ( 2 x. ( A x. q ) ) ) ) = ( ( q ^ 2 ) - ( r ^ 2 ) ) ) )
82 76 81 mpbid 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( A ^ 2 ) - ( 2 x. ( A x. r ) ) ) - ( ( A ^ 2 ) - ( 2 x. ( A x. q ) ) ) ) = ( ( q ^ 2 ) - ( r ^ 2 ) ) )
83 61 65 82 3eqtr2d 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( 2 x. ( ( A x. q ) - ( A x. r ) ) ) = ( ( q ^ 2 ) - ( r ^ 2 ) ) )
84 78 80 subcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( q ^ 2 ) - ( r ^ 2 ) ) e. CC )
85 56 60 subcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( A x. q ) - ( A x. r ) ) e. CC )
86 2ne0 
 |-  2 =/= 0
87 86 a1i 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> 2 =/= 0 )
88 84 50 85 87 divmuld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) = ( ( A x. q ) - ( A x. r ) ) <-> ( 2 x. ( ( A x. q ) - ( A x. r ) ) ) = ( ( q ^ 2 ) - ( r ^ 2 ) ) ) )
89 83 88 mpbird 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) = ( ( A x. q ) - ( A x. r ) ) )
90 52 55 59 subdid 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( A x. ( q - r ) ) = ( ( A x. q ) - ( A x. r ) ) )
91 89 90 eqtr4d 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) = ( A x. ( q - r ) ) )
92 84 halfcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) e. CC )
93 55 59 subcld 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( q - r ) e. CC )
94 simprl 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> q =/= r )
95 55 59 94 subne0d 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( q - r ) =/= 0 )
96 92 52 93 95 divmul3d 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) / ( q - r ) ) = A <-> ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) = ( A x. ( q - r ) ) ) )
97 91 96 mpbird 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) / ( q - r ) ) = A )
98 qsqcl 
 |-  ( q e. QQ -> ( q ^ 2 ) e. QQ )
99 53 98 syl 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( q ^ 2 ) e. QQ )
100 qsqcl 
 |-  ( r e. QQ -> ( r ^ 2 ) e. QQ )
101 57 100 syl 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( r ^ 2 ) e. QQ )
102 qsubcl 
 |-  ( ( ( q ^ 2 ) e. QQ /\ ( r ^ 2 ) e. QQ ) -> ( ( q ^ 2 ) - ( r ^ 2 ) ) e. QQ )
103 99 101 102 syl2anc 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( q ^ 2 ) - ( r ^ 2 ) ) e. QQ )
104 2z 
 |-  2 e. ZZ
105 zq 
 |-  ( 2 e. ZZ -> 2 e. QQ )
106 104 105 mp1i 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> 2 e. QQ )
107 qdivcl 
 |-  ( ( ( ( q ^ 2 ) - ( r ^ 2 ) ) e. QQ /\ 2 e. QQ /\ 2 =/= 0 ) -> ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) e. QQ )
108 103 106 87 107 syl3anc 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) e. QQ )
109 qsubcl 
 |-  ( ( q e. QQ /\ r e. QQ ) -> ( q - r ) e. QQ )
110 53 57 109 syl2anc 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( q - r ) e. QQ )
111 qdivcl 
 |-  ( ( ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) e. QQ /\ ( q - r ) e. QQ /\ ( q - r ) =/= 0 ) -> ( ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) / ( q - r ) ) e. QQ )
112 108 110 95 111 syl3anc 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> ( ( ( ( q ^ 2 ) - ( r ^ 2 ) ) / 2 ) / ( q - r ) ) e. QQ )
113 97 112 eqeltrrd 
 |-  ( ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) /\ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) -> A e. QQ )
114 113 ex 
 |-  ( ( A e. RR /\ ( q e. QQ /\ r e. QQ ) ) -> ( ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) -> A e. QQ ) )
115 114 rexlimdvva 
 |-  ( A e. RR -> ( E. q e. QQ E. r e. QQ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) -> A e. QQ ) )
116 49 115 impbid2 
 |-  ( A e. RR -> ( A e. QQ <-> E. q e. QQ E. r e. QQ ( q =/= r /\ ( abs ` ( A - q ) ) = ( abs ` ( A - r ) ) ) ) )