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 \in ℝ \to (A \in ℚ \leftrightarrow \exists q \in ℚ \exists r \in ℚ (q \neq r \land \|A - q\| = \|A - r\|))$

Proof

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

Metamath Proof Explorer

Theorem qdiff

Proof