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

Proof

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